From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Core/ResolutionContext.cs | 1270 +++++++++++++++++++------------------- 1 file changed, 641 insertions(+), 629 deletions(-) (limited to 'Source/Core/ResolutionContext.cs') diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index bf1a5629..279e00bf 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -1,629 +1,641 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -namespace Microsoft.Boogie { - using System.Collections; - using System.Collections.Generic; - using System; - using System.Linq; - using System.Diagnostics.Contracts; - - [ContractClass(typeof(IErrorSinkContracts))] - public interface IErrorSink { - void Error(IToken/*!*/ tok, string/*!*/ msg); - } - [ContractClassFor(typeof(IErrorSink))] - public abstract class IErrorSinkContracts : IErrorSink { - #region IErrorSink Members - public void Error(IToken tok, string msg) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); - throw new NotImplementedException(); - } - #endregion - } - - public class CheckingContext { - // ------------------------------ Error counting ------------------------------ - - IErrorSink errorSink; - int errors; - - public CheckingContext(IErrorSink errorSink) { - this.errorSink = errorSink; - } - - public int ErrorCount { - get { - return errors; - } - set { - errors = value; - } - } - - public void Error(Absy subject, string msg, params object[] args) { - Contract.Requires(args != null); - Contract.Requires(msg != null); - Contract.Requires(subject != null); - Error(subject.tok, msg, args); - } - - public virtual void Error(IToken tok, string msg) { - Contract.Requires(msg != null); - Contract.Requires(tok != null); - errors++; - if (errorSink == null) { - ConsoleColor col = Console.ForegroundColor; - Console.ForegroundColor = ConsoleColor.Red; - Console.WriteLine("{0}({1},{2}): Error: {3}", - tok.filename, tok.line, tok.col - 1, - msg); - Console.ForegroundColor = col; - } else { - errorSink.Error(tok, msg); - } - } - - private string Format(string msg, params object[] args) { - Contract.Requires(msg != null); - Contract.Ensures(Contract.Result() != null); - if (System.Type.GetType("Mono.Runtime") != null) { // MONO - // something in mono seems to be broken so that calling - // NamedDeclarations.ToString (and similar ToString methods) - // causes a stack overflow. We therefore convert those to - // strings by hand - object[] fixedArgs = new object[cce.NonNull(args).Length]; - for (int i = 0; i < args.Length; ++i) { - if (args[i] is NamedDeclaration) { - fixedArgs[i] = cce.NonNull((NamedDeclaration)args[i]).Name; - } else if (args[i] is Type) { - System.IO.StringWriter buffer = new System.IO.StringWriter(); - using (TokenTextWriter stream = new TokenTextWriter("", buffer, /*setTokens=*/ false, /*pretty=*/ false)) { - cce.NonNull((Type)args[i]).Emit(stream); - } - fixedArgs[i] = buffer.ToString(); - } else if (args[i] is Expr) { - System.IO.StringWriter buffer = new System.IO.StringWriter(); - using (TokenTextWriter stream = new TokenTextWriter("", buffer, /*setTokens=*/ false, /*pretty=*/ false)) { - cce.NonNull((Expr/*!*/)args[i]).Emit(stream, 0, false); - } - fixedArgs[i] = buffer.ToString(); - } else { - fixedArgs[i] = args[i]; - } - } - args = fixedArgs; - } - return string.Format(msg, args); - } - - public void Error(IToken tok, string msg, params object[] args) { - Contract.Requires(msg != null); - Contract.Requires(tok != null); - Error(tok, Format(msg, args)); - } - - public void Warning(Absy subject, string msg, params object[] args) { - Contract.Requires(args != null); - Contract.Requires(msg != null); - Contract.Requires(subject != null); - Warning(subject.tok, msg, args); - } - - public virtual void Warning(IToken tok, string msg) { - Contract.Requires(msg != null); - Contract.Requires(tok != null); - // warnings are currently always written to the console - ConsoleColor col = Console.ForegroundColor; - Console.ForegroundColor = ConsoleColor.DarkYellow; - Console.WriteLine("{0}({1},{2}): Warning: {3}", - tok.filename, tok.line, tok.col - 1, - msg); - Console.ForegroundColor = col; - } - - public void Warning(IToken tok, string msg, params object[] args) { - Contract.Requires(msg != null); - Contract.Requires(tok != null); - Warning(tok, Format(msg, args)); - } - } - - public class ResolutionContext : CheckingContext { - public ResolutionContext(IErrorSink errorSink) - : base(errorSink) { - } - - // ------------------------------ Boogie 2 Types ------------------------- - - // user-defined types, which can be either TypeCtorDecl or TypeSynonymDecl - Hashtable /*string->NamedDeclaration*//*!*/ types = new Hashtable /*string->NamedDeclaration*/ (); - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(types != null); - Contract.Invariant(cce.NonNullElements(typeBinders)); - Contract.Invariant(varContext != null); - Contract.Invariant(funcdures != null); - } - - - /// - /// Checks if name coincides with the name of a bitvector type. If so, reports an error and - /// returns true; otherwise, returns false. - /// - private bool CheckBvNameClashes(Absy absy, string name) { - Contract.Requires(name != null); - Contract.Requires(absy != null); - if (name.StartsWith("bv") && name.Length > 2) { - for (int i = 2; i < name.Length; ++i) - if (!char.IsDigit(name[i])) - return false; - Error(absy, "type name: {0} is registered for bitvectors", name); - return true; - } - return false; - } - - public void AddType(NamedDeclaration td) { - Contract.Requires(td != null); - Contract.Requires((td is TypeCtorDecl) || (td is TypeSynonymDecl)); - Contract.Requires(td.Name != null); - - string name = td.Name; - if (CheckBvNameClashes(td, name)) - return; // error has already been reported - - var previous = (NamedDeclaration)types[name]; - if (previous == null) { - types.Add(name, td); - } else { - var r = (NamedDeclaration)SelectNonExtern(td, previous); - if (r == null) { - Error(td, "more than one declaration of type name: {0}", name); - } else { - types[name] = r; - } - } - } - - /// - /// Returns the declaration of the named type, or null if - /// no such type is declared. Also return null if the type - /// declared with the given name is not a constructor but a - /// type synonym - /// - /// - /// - public TypeCtorDecl LookUpType(string name) { - Contract.Requires(name != null); - return types[name] as TypeCtorDecl; - } - - public TypeSynonymDecl LookUpTypeSynonym(string name) { - Contract.Requires(name != null); - return types[name] as TypeSynonymDecl; - } - - // ------------------------------ Boogie 2 Type Binders ------------------------------ - - List/*!*/ typeBinders = new List(5); - - public void AddTypeBinder(TypeVariable td) { - Contract.Requires(td != null); - if (CheckBvNameClashes(td, td.Name)) { - return; - } - if (types.ContainsKey(td.Name)) { - Error(td, "name is already reserved for type constructor: {0}", td.Name); - return; - } - for (int i = 0; i < typeBinders.Count; i++) { - if (typeBinders[i].Name == td.Name) { - Error(td, "more than one declaration of type variable: {0}", td.Name); - return; - } - } - typeBinders.Add(td); - } - - public int TypeBinderState { - get { - return typeBinders.Count; - } - set { - typeBinders.RemoveRange(value, typeBinders.Count - value); - } - } - - /// - /// Returns the declaration of the named type binder, or null if - /// no such binder is declared. - /// - public TypeVariable LookUpTypeBinder(string name) { - Contract.Requires(name != null); - for (int i = typeBinders.Count; 0 <= --i; ) { - TypeVariable/*!*/ td = typeBinders[i]; - Contract.Assert(td != null); - if (td.Name == name) { - return td; - } - } - return null; // not present - } - - // ------------------------------ Variables ------------------------------ - - class VarContextNode { - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(VarSymbols != null); - } - - public readonly Hashtable /*string->Variable*//*!*/ VarSymbols = new Hashtable /*string->Variable*/(); - public /*maybe null*/ VarContextNode ParentContext; - public readonly bool Opaque; - readonly ISet assignedAssumptionVariables = new HashSet(); - - public bool HasVariableBeenAssigned(string name) - { - Contract.Requires(name != null); - - if (assignedAssumptionVariables.Contains(name)) - { - return true; - } - else if (ParentContext != null) - { - return ParentContext.HasVariableBeenAssigned(name); - } - else - { - return false; - } - } - - public bool MarkVariableAsAssigned(string name) - { - Contract.Requires(name != null); - - if (VarSymbols.Contains(name)) - { - if (assignedAssumptionVariables.Contains(name)) - { - return false; - } - assignedAssumptionVariables.Add(name); - return true; - } - else if (ParentContext != null) - { - return ParentContext.MarkVariableAsAssigned(name); - } - else - { - return false; - } - } - - public VarContextNode(/*maybe null*/ VarContextNode parentContext, bool opaque) { - ParentContext = parentContext; - Opaque = opaque; - } - } - - // symbolic constants, global variables, local variables, formals, expression-bound variables - VarContextNode/*!*/ varContext = new VarContextNode(null, false); - - /// - /// Adds a variable context. - /// - public void PushVarContext() { - varContext = new VarContextNode(varContext, false); - } - - /// - /// Adds an opaque variable context, that is, one that blocks all previously pushed contexts. - /// - public void PushOpaqueVarContext() { - varContext = new VarContextNode(varContext, true); - } - - /// - /// Requires there to be more than one variable context. - /// - public void PopVarContext() { - Contract.Assert(varContext.ParentContext != null); - varContext = varContext.ParentContext; - } - - public void AddVariable(Variable var, bool global) { - Contract.Requires(var != null); - var previous = FindVariable(cce.NonNull(var.Name), !global); - if (previous == null) { - varContext.VarSymbols.Add(var.Name, var); - } else { - var r = (Variable)SelectNonExtern(var, previous); - if (r == null) { - Error(var, "more than one declaration of variable name: {0}", var.Name); - } else { - varContext.VarSymbols[var.Name] = r; - } - } - } - - /// - /// Returns the declaration of the named variable, or null if - /// no such variable is declared. - /// - /// - /// - public Variable LookUpVariable(string name) { - Contract.Requires(name != null); - return FindVariable(name, false); - } - - Variable FindVariable(string name, bool ignoreTopLevelVars) { - Contract.Requires(name != null); - VarContextNode c = varContext; - bool lookOnlyForConstants = false; - do { - if (ignoreTopLevelVars && c.ParentContext == null) { - // this is the top level and we're asked to ignore the top level; hence, we're done - break; - } - - Variable var = (Variable)c.VarSymbols[name]; - if (var != null && (!lookOnlyForConstants || var is Constant)) { - return var; - } - // not at this level - - if (c.Opaque) { - // from here on, only constants can be looked up - lookOnlyForConstants = true; - } - c = c.ParentContext; - } while (c != null); - - // not present in the relevant levels - return null; - } - - public bool HasVariableBeenAssigned(string name) - { - Contract.Requires(name != null); - - return varContext.HasVariableBeenAssigned(name); - } - - public void MarkVariableAsAssigned(string name) - { - Contract.Requires(name != null); - - var success = varContext.MarkVariableAsAssigned(name); - Contract.Assume(success); - } - - Hashtable axioms = new Hashtable(); - - public void AddAxiom(Axiom axiom) { - string axiomName = QKeyValue.FindStringAttribute(axiom.Attributes, "name"); - if (axiomName == null) - return; - var previous = (Axiom)axioms[axiomName]; - if (previous == null) { - axioms.Add(axiomName, axiom); - } - else { - var r = (Axiom)SelectNonExtern(axiom, previous); - if (r == null) { - Error(axiom, "more than one declaration of axiom name: {0}", axiomName); - } - else { - axioms[axiomName] = r; - } - } - } - - // ------------------------------ Functions/Procedures ------------------------------ - - // uninterpreted function symbols, procedures - Hashtable /*string->DeclWithFormals*//*!*/ funcdures = new Hashtable /*string->DeclWithFormals*/ (); - - public void AddProcedure(DeclWithFormals proc) { - Contract.Requires(proc != null); - Contract.Requires(proc.Name != null); - - string name = proc.Name; - var previous = (DeclWithFormals)funcdures[name]; - if (previous == null) { - funcdures.Add(name, proc); - } else { - var r = (DeclWithFormals)SelectNonExtern(proc, previous); - if (r == null) { - Error(proc, "more than one declaration of function/procedure name: {0}", name); - } else { - funcdures[name] = r; - } - } - } - - /// - /// If both "a" and "b" have an ":extern" attribute, returns either one. - /// If one of "a" and "b" has an ":extern" attribute, returns that one. - /// If neither of "a" and "b" has an ":extern" attribute, returns null. - /// If a non-value value is returned, this method also adds the ":ignore" - /// attribute to the declaration NOT returned. - /// - Declaration SelectNonExtern(Declaration a, Declaration b) { - Contract.Requires(a != null); - Contract.Requires(b != null); - Contract.Ensures(Contract.Result() == null || Contract.Result() == a || Contract.Result() == b); - - Declaration ignore, keep; - if (QKeyValue.FindBoolAttribute(a.Attributes, "extern")) { - ignore = a; - keep = b; - } else if (QKeyValue.FindBoolAttribute(b.Attributes, "extern")) { - ignore = b; - keep = a; - } else { - return null; - } - // prepend :ignore attribute - ignore.Attributes = new QKeyValue(ignore.tok, "ignore", new List(), ignore.Attributes); - return keep; - } - - /// - /// Returns the declaration of the named function/procedure, or null if - /// no such function or procedure is declared. - /// - /// - /// - public DeclWithFormals LookUpProcedure(string name) { - Contract.Requires(name != null); - return (DeclWithFormals)funcdures[name]; - } - - // ------------------------------ Blocks ------------------------------ - - class ProcedureContext { - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Blocks != null); - } - - public readonly Hashtable/*!*/ /*string->Block!*/ Blocks; - public readonly ProcedureContext Next; - public ProcedureContext(ProcedureContext next) { - Blocks = new Hashtable /*string->Block!*/ (); - Next = next; - } - } - /*maybe null*/ - ProcedureContext procedureContext; // stack of procedure contexts - public bool HasProcedureContext { - get { - return procedureContext != null; - } - } - - /// - /// Pushes a new procedure context. - /// - public void PushProcedureContext() { - Contract.Ensures(HasProcedureContext); - procedureContext = new ProcedureContext(procedureContext); - } - - /// - /// Requires there to be a procedure context. Pops it. - /// - public void PopProcedureContext() { - Contract.Requires(HasProcedureContext); - Contract.Assert(procedureContext != null); // follows from precondition - procedureContext = procedureContext.Next; - } - - /// - /// Requires there to be a procedure context. - /// - /// - public void AddBlock(Block block) { - Contract.Requires(block != null); - Contract.Requires(HasProcedureContext); - Contract.Assert(procedureContext != null); // follows from precondition - Hashtable/*!*/ /*string->Block!*/ blocks = procedureContext.Blocks; - Contract.Assert(blocks != null); - if (blocks[block.Label] != null) { - Error(block, "more than one declaration of block name: {0}", block.Label); - } else { - blocks.Add(block.Label, block); - } - } - - /// - /// Requires there to be a procedure context. - /// Returns the declaration of the named block, or null if - /// no such block is declared. - /// - /// - /// - public Block LookUpBlock(string name) { - Contract.Requires(name != null); - Contract.Requires(HasProcedureContext); - Contract.Assert(procedureContext != null); // follows from precondition - Hashtable/*!*/ /*string->Block!*/ blocks = procedureContext.Blocks; - Contract.Assert(blocks != null); - return (Block)blocks[name]; - } - - // ------------------------------ Flags ------------------------------ - - public enum State { - StateLess, - Single, - Two - } - State stateMode = State.Single; - - /// - /// To increase our confidence in that the caller knows what it's doing, we only allow - /// the state mode to be changed in and out of the State.Single mode. - /// - public State StateMode { - get { - return stateMode; - } - set { - Contract.Assert(value != stateMode); - Contract.Assert(stateMode == State.Single || value == State.Single); - cce.BeginExpose(this); - { - stateMode = value; - } - cce.EndExpose(); - } - } - - bool triggerMode = false; - - /// - /// Setting TriggerMode is allowed only if the setting has the effect of toggling the - /// boolean. That is, TriggerMode can be set to true only if it previously was false, - /// and TriggerMode can be set to false only if it previously was true. - /// - public bool TriggerMode { - get { - return triggerMode; - } - set { - Contract.Assert(triggerMode != value); - cce.BeginExpose(this); - { - triggerMode = value; - } - cce.EndExpose(); - } - } - } - - public class TypecheckingContext : CheckingContext { - public List Frame; // used in checking the assignment targets of implementation bodies - public bool Yields; - - public TypecheckingContext(IErrorSink errorSink) - : base(errorSink) { - } - - public bool InFrame(Variable v) { - Contract.Requires(v != null); - Contract.Requires(Frame != null); - return Frame.Any(f => f.Decl == v); - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.Boogie { + using System.Collections; + using System.Collections.Generic; + using System; + using System.Linq; + using System.Diagnostics.Contracts; + + [ContractClass(typeof(IErrorSinkContracts))] + public interface IErrorSink { + void Error(IToken/*!*/ tok, string/*!*/ msg); + } + [ContractClassFor(typeof(IErrorSink))] + public abstract class IErrorSinkContracts : IErrorSink { + #region IErrorSink Members + public void Error(IToken tok, string msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + throw new NotImplementedException(); + } + #endregion + } + + public class CheckingContext { + // ------------------------------ Error counting ------------------------------ + + IErrorSink errorSink; + int errors; + + public CheckingContext(IErrorSink errorSink) { + this.errorSink = errorSink; + } + + public int ErrorCount { + get { + return errors; + } + set { + errors = value; + } + } + + public void Error(Absy subject, string msg, params object[] args) { + Contract.Requires(args != null); + Contract.Requires(msg != null); + Contract.Requires(subject != null); + Error(subject.tok, msg, args); + } + + public virtual void Error(IToken tok, string msg) { + Contract.Requires(msg != null); + Contract.Requires(tok != null); + errors++; + if (errorSink == null) { + ConsoleColor col = Console.ForegroundColor; + Console.ForegroundColor = ConsoleColor.Red; + Console.WriteLine("{0}({1},{2}): Error: {3}", + tok.filename, tok.line, tok.col - 1, + msg); + Console.ForegroundColor = col; + } else { + errorSink.Error(tok, msg); + } + } + + private string Format(string msg, params object[] args) { + Contract.Requires(msg != null); + Contract.Ensures(Contract.Result() != null); + if (System.Type.GetType("Mono.Runtime") != null) { // MONO + // something in mono seems to be broken so that calling + // NamedDeclarations.ToString (and similar ToString methods) + // causes a stack overflow. We therefore convert those to + // strings by hand + object[] fixedArgs = new object[cce.NonNull(args).Length]; + for (int i = 0; i < args.Length; ++i) { + if (args[i] is NamedDeclaration) { + fixedArgs[i] = cce.NonNull((NamedDeclaration)args[i]).Name; + } else if (args[i] is Type) { + System.IO.StringWriter buffer = new System.IO.StringWriter(); + using (TokenTextWriter stream = new TokenTextWriter("", buffer, /*setTokens=*/ false, /*pretty=*/ false)) { + cce.NonNull((Type)args[i]).Emit(stream); + } + fixedArgs[i] = buffer.ToString(); + } else if (args[i] is Expr) { + System.IO.StringWriter buffer = new System.IO.StringWriter(); + using (TokenTextWriter stream = new TokenTextWriter("", buffer, /*setTokens=*/ false, /*pretty=*/ false)) { + cce.NonNull((Expr/*!*/)args[i]).Emit(stream, 0, false); + } + fixedArgs[i] = buffer.ToString(); + } else { + fixedArgs[i] = args[i]; + } + } + args = fixedArgs; + } + return string.Format(msg, args); + } + + public void Error(IToken tok, string msg, params object[] args) { + Contract.Requires(msg != null); + Contract.Requires(tok != null); + Error(tok, Format(msg, args)); + } + + public void Warning(Absy subject, string msg, params object[] args) { + Contract.Requires(args != null); + Contract.Requires(msg != null); + Contract.Requires(subject != null); + Warning(subject.tok, msg, args); + } + + public virtual void Warning(IToken tok, string msg) { + Contract.Requires(msg != null); + Contract.Requires(tok != null); + // warnings are currently always written to the console + ConsoleColor col = Console.ForegroundColor; + Console.ForegroundColor = ConsoleColor.DarkYellow; + Console.WriteLine("{0}({1},{2}): Warning: {3}", + tok.filename, tok.line, tok.col - 1, + msg); + Console.ForegroundColor = col; + } + + public void Warning(IToken tok, string msg, params object[] args) { + Contract.Requires(msg != null); + Contract.Requires(tok != null); + Warning(tok, Format(msg, args)); + } + } + + public class ResolutionContext : CheckingContext { + public ResolutionContext(IErrorSink errorSink) + : base(errorSink) { + } + + // ------------------------------ Boogie 2 Types ------------------------- + + // user-defined types, which can be either TypeCtorDecl or TypeSynonymDecl + Hashtable /*string->NamedDeclaration*//*!*/ types = new Hashtable /*string->NamedDeclaration*/ (); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(types != null); + Contract.Invariant(cce.NonNullElements(typeBinders)); + Contract.Invariant(varContext != null); + Contract.Invariant(funcdures != null); + } + + + /// + /// Checks if name coincides with the name of a bitvector type. If so, reports an error and + /// returns true; otherwise, returns false. + /// + private bool CheckBvNameClashes(Absy absy, string name) { + Contract.Requires(name != null); + Contract.Requires(absy != null); + if (name.StartsWith("bv") && name.Length > 2) { + for (int i = 2; i < name.Length; ++i) + if (!char.IsDigit(name[i])) + return false; + Error(absy, "type name: {0} is registered for bitvectors", name); + return true; + } + return false; + } + + public void AddType(NamedDeclaration td) { + Contract.Requires(td != null); + Contract.Requires((td is TypeCtorDecl) || (td is TypeSynonymDecl)); + Contract.Requires(td.Name != null); + + string name = td.Name; + if (CheckBvNameClashes(td, name)) + return; // error has already been reported + + var previous = (NamedDeclaration)types[name]; + if (previous == null) { + types.Add(name, td); + } else { + var r = (NamedDeclaration)SelectNonExtern(td, previous); + if (r == null) { + Error(td, "more than one declaration of type name: {0}", name); + } else { + types[name] = r; + } + } + } + + /// + /// Returns the declaration of the named type, or null if + /// no such type is declared. Also return null if the type + /// declared with the given name is not a constructor but a + /// type synonym + /// + /// + /// + public TypeCtorDecl LookUpType(string name) { + Contract.Requires(name != null); + return types[name] as TypeCtorDecl; + } + + public TypeSynonymDecl LookUpTypeSynonym(string name) { + Contract.Requires(name != null); + return types[name] as TypeSynonymDecl; + } + + // ------------------------------ Boogie 2 Type Binders ------------------------------ + + List/*!*/ typeBinders = new List(5); + + public void AddTypeBinder(TypeVariable td) { + Contract.Requires(td != null); + if (CheckBvNameClashes(td, td.Name)) { + return; + } + if (types.ContainsKey(td.Name)) { + Error(td, "name is already reserved for type constructor: {0}", td.Name); + return; + } + for (int i = 0; i < typeBinders.Count; i++) { + if (typeBinders[i].Name == td.Name) { + Error(td, "more than one declaration of type variable: {0}", td.Name); + return; + } + } + typeBinders.Add(td); + } + + public int TypeBinderState { + get { + return typeBinders.Count; + } + set { + typeBinders.RemoveRange(value, typeBinders.Count - value); + } + } + + /// + /// Returns the declaration of the named type binder, or null if + /// no such binder is declared. + /// + public TypeVariable LookUpTypeBinder(string name) { + Contract.Requires(name != null); + for (int i = typeBinders.Count; 0 <= --i; ) { + TypeVariable/*!*/ td = typeBinders[i]; + Contract.Assert(td != null); + if (td.Name == name) { + return td; + } + } + return null; // not present + } + + // ------------------------------ Variables ------------------------------ + + class VarContextNode { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(VarSymbols != null); + } + + public readonly Hashtable /*string->Variable*//*!*/ VarSymbols = new Hashtable /*string->Variable*/(); + public /*maybe null*/ VarContextNode ParentContext; + public readonly bool Opaque; + readonly ISet assignedAssumptionVariables = new HashSet(); + + public bool HasVariableBeenAssigned(string name) + { + Contract.Requires(name != null); + + if (assignedAssumptionVariables.Contains(name)) + { + return true; + } + else if (ParentContext != null) + { + return ParentContext.HasVariableBeenAssigned(name); + } + else + { + return false; + } + } + + public bool MarkVariableAsAssigned(string name) + { + Contract.Requires(name != null); + + if (VarSymbols.Contains(name)) + { + if (assignedAssumptionVariables.Contains(name)) + { + return false; + } + assignedAssumptionVariables.Add(name); + return true; + } + else if (ParentContext != null) + { + return ParentContext.MarkVariableAsAssigned(name); + } + else + { + return false; + } + } + + public VarContextNode(/*maybe null*/ VarContextNode parentContext, bool opaque) { + ParentContext = parentContext; + Opaque = opaque; + } + } + + // symbolic constants, global variables, local variables, formals, expression-bound variables + VarContextNode/*!*/ varContext = new VarContextNode(null, false); + + /// + /// Adds a variable context. + /// + public void PushVarContext() { + varContext = new VarContextNode(varContext, false); + } + + /// + /// Adds an opaque variable context, that is, one that blocks all previously pushed contexts. + /// + public void PushOpaqueVarContext() { + varContext = new VarContextNode(varContext, true); + } + + /// + /// Requires there to be more than one variable context. + /// + public void PopVarContext() { + Contract.Assert(varContext.ParentContext != null); + varContext = varContext.ParentContext; + } + + public readonly ISet StatementIds = new HashSet(); + + public void AddStatementId(IToken tok, string name) + { + if (StatementIds.Contains(name)) + { + Error(tok, "more than one statement with same id: " + name); + return; + } + StatementIds.Add(name); + } + + public void AddVariable(Variable var, bool global) { + Contract.Requires(var != null); + var previous = FindVariable(cce.NonNull(var.Name), !global); + if (previous == null) { + varContext.VarSymbols.Add(var.Name, var); + } else { + var r = (Variable)SelectNonExtern(var, previous); + if (r == null) { + Error(var, "more than one declaration of variable name: {0}", var.Name); + } else { + varContext.VarSymbols[var.Name] = r; + } + } + } + + /// + /// Returns the declaration of the named variable, or null if + /// no such variable is declared. + /// + /// + /// + public Variable LookUpVariable(string name) { + Contract.Requires(name != null); + return FindVariable(name, false); + } + + Variable FindVariable(string name, bool ignoreTopLevelVars) { + Contract.Requires(name != null); + VarContextNode c = varContext; + bool lookOnlyForConstants = false; + do { + if (ignoreTopLevelVars && c.ParentContext == null) { + // this is the top level and we're asked to ignore the top level; hence, we're done + break; + } + + Variable var = (Variable)c.VarSymbols[name]; + if (var != null && (!lookOnlyForConstants || var is Constant)) { + return var; + } + // not at this level + + if (c.Opaque) { + // from here on, only constants can be looked up + lookOnlyForConstants = true; + } + c = c.ParentContext; + } while (c != null); + + // not present in the relevant levels + return null; + } + + public bool HasVariableBeenAssigned(string name) + { + Contract.Requires(name != null); + + return varContext.HasVariableBeenAssigned(name); + } + + public void MarkVariableAsAssigned(string name) + { + Contract.Requires(name != null); + + var success = varContext.MarkVariableAsAssigned(name); + Contract.Assume(success); + } + + Hashtable axioms = new Hashtable(); + + public void AddAxiom(Axiom axiom) { + string axiomName = QKeyValue.FindStringAttribute(axiom.Attributes, "name"); + if (axiomName == null) + return; + var previous = (Axiom)axioms[axiomName]; + if (previous == null) { + axioms.Add(axiomName, axiom); + } + else { + var r = (Axiom)SelectNonExtern(axiom, previous); + if (r == null) { + Error(axiom, "more than one declaration of axiom name: {0}", axiomName); + } + else { + axioms[axiomName] = r; + } + } + } + + // ------------------------------ Functions/Procedures ------------------------------ + + // uninterpreted function symbols, procedures + Hashtable /*string->DeclWithFormals*//*!*/ funcdures = new Hashtable /*string->DeclWithFormals*/ (); + + public void AddProcedure(DeclWithFormals proc) { + Contract.Requires(proc != null); + Contract.Requires(proc.Name != null); + + string name = proc.Name; + var previous = (DeclWithFormals)funcdures[name]; + if (previous == null) { + funcdures.Add(name, proc); + } else { + var r = (DeclWithFormals)SelectNonExtern(proc, previous); + if (r == null) { + Error(proc, "more than one declaration of function/procedure name: {0}", name); + } else { + funcdures[name] = r; + } + } + } + + /// + /// If both "a" and "b" have an ":extern" attribute, returns either one. + /// If one of "a" and "b" has an ":extern" attribute, returns that one. + /// If neither of "a" and "b" has an ":extern" attribute, returns null. + /// If a non-value value is returned, this method also adds the ":ignore" + /// attribute to the declaration NOT returned. + /// + Declaration SelectNonExtern(Declaration a, Declaration b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Ensures(Contract.Result() == null || Contract.Result() == a || Contract.Result() == b); + + Declaration ignore, keep; + if (QKeyValue.FindBoolAttribute(a.Attributes, "extern")) { + ignore = a; + keep = b; + } else if (QKeyValue.FindBoolAttribute(b.Attributes, "extern")) { + ignore = b; + keep = a; + } else { + return null; + } + // prepend :ignore attribute + ignore.Attributes = new QKeyValue(ignore.tok, "ignore", new List(), ignore.Attributes); + return keep; + } + + /// + /// Returns the declaration of the named function/procedure, or null if + /// no such function or procedure is declared. + /// + /// + /// + public DeclWithFormals LookUpProcedure(string name) { + Contract.Requires(name != null); + return (DeclWithFormals)funcdures[name]; + } + + // ------------------------------ Blocks ------------------------------ + + class ProcedureContext { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Blocks != null); + } + + public readonly Hashtable/*!*/ /*string->Block!*/ Blocks; + public readonly ProcedureContext Next; + public ProcedureContext(ProcedureContext next) { + Blocks = new Hashtable /*string->Block!*/ (); + Next = next; + } + } + /*maybe null*/ + ProcedureContext procedureContext; // stack of procedure contexts + public bool HasProcedureContext { + get { + return procedureContext != null; + } + } + + /// + /// Pushes a new procedure context. + /// + public void PushProcedureContext() { + Contract.Ensures(HasProcedureContext); + procedureContext = new ProcedureContext(procedureContext); + } + + /// + /// Requires there to be a procedure context. Pops it. + /// + public void PopProcedureContext() { + Contract.Requires(HasProcedureContext); + Contract.Assert(procedureContext != null); // follows from precondition + procedureContext = procedureContext.Next; + } + + /// + /// Requires there to be a procedure context. + /// + /// + public void AddBlock(Block block) { + Contract.Requires(block != null); + Contract.Requires(HasProcedureContext); + Contract.Assert(procedureContext != null); // follows from precondition + Hashtable/*!*/ /*string->Block!*/ blocks = procedureContext.Blocks; + Contract.Assert(blocks != null); + if (blocks[block.Label] != null) { + Error(block, "more than one declaration of block name: {0}", block.Label); + } else { + blocks.Add(block.Label, block); + } + } + + /// + /// Requires there to be a procedure context. + /// Returns the declaration of the named block, or null if + /// no such block is declared. + /// + /// + /// + public Block LookUpBlock(string name) { + Contract.Requires(name != null); + Contract.Requires(HasProcedureContext); + Contract.Assert(procedureContext != null); // follows from precondition + Hashtable/*!*/ /*string->Block!*/ blocks = procedureContext.Blocks; + Contract.Assert(blocks != null); + return (Block)blocks[name]; + } + + // ------------------------------ Flags ------------------------------ + + public enum State { + StateLess, + Single, + Two + } + State stateMode = State.Single; + + /// + /// To increase our confidence in that the caller knows what it's doing, we only allow + /// the state mode to be changed in and out of the State.Single mode. + /// + public State StateMode { + get { + return stateMode; + } + set { + Contract.Assert(value != stateMode); + Contract.Assert(stateMode == State.Single || value == State.Single); + cce.BeginExpose(this); + { + stateMode = value; + } + cce.EndExpose(); + } + } + + bool triggerMode = false; + + /// + /// Setting TriggerMode is allowed only if the setting has the effect of toggling the + /// boolean. That is, TriggerMode can be set to true only if it previously was false, + /// and TriggerMode can be set to false only if it previously was true. + /// + public bool TriggerMode { + get { + return triggerMode; + } + set { + Contract.Assert(triggerMode != value); + cce.BeginExpose(this); + { + triggerMode = value; + } + cce.EndExpose(); + } + } + } + + public class TypecheckingContext : CheckingContext { + public List Frame; // used in checking the assignment targets of implementation bodies + public bool Yields; + + public TypecheckingContext(IErrorSink errorSink) + : base(errorSink) { + } + + public bool InFrame(Variable v) { + Contract.Requires(v != null); + Contract.Requires(Frame != null); + return Frame.Any(f => f.Decl == v); + } + } +} -- cgit v1.2.3