diff options
| author |  tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
| commit | b617dda87871573b826dada4af73fc48dce94f15 (patch) | |
| tree | 453088d59b99376c0b14035e76463a4561d6ec1c /Source/Core/ResolutionContext.cs | |
| parent | 0d77cf304b9bd2b2152fe1a733e4533536c883c0 (diff) | |
Boogie: Renaming core sources in preparation for port commit
Diffstat (limited to 'Source/Core/ResolutionContext.cs')
| -rw-r--r-- | Source/Core/ResolutionContext.cs | 539 |
1 files changed, 539 insertions, 0 deletions
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs new file mode 100644 index 00000000..10ff7d87 --- /dev/null +++ b/Source/Core/ResolutionContext.cs @@ -0,0 +1,539 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie
+{
+ using System.Collections;
+ using System.Collections.Generic;
+ using System;
+ using Microsoft.SpecSharp.Collections;
+ using Microsoft.Contracts;
+
+ public interface IErrorSink
+ {
+ void Error(IToken! tok, string! msg);
+ }
+
+ 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)
+ {
+ Error(subject.tok, msg, args);
+ }
+
+ public virtual void Error(IToken! tok, string! msg)
+ {
+ 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) {
+ 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 [((!)args).Length];
+ for (int i = 0; i < args.Length; ++i) {
+ if (args[i] is NamedDeclaration) {
+ fixedArgs[i] = ((NamedDeclaration!)args[i]).Name;
+ } else if (args[i] is Type) {
+ System.IO.StringWriter buffer = new System.IO.StringWriter();
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
+ ((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>", buffer, false)) {
+ ((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)
+ {
+ Error(tok, Format(msg, args));
+ }
+
+ public void Warning(Absy! subject, string! msg, params object[]! args)
+ {
+ Warning(subject.tok, msg, args);
+ }
+
+ public virtual void Warning(IToken! tok, string! msg)
+ {
+ // 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)
+ {
+ 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*/ ();
+
+ /// <summary>
+ /// Checks if name coincides with the name of a bitvector type. If so, reports an error and
+ /// returns true; otherwise, returns false.
+ /// </summary>
+ private bool CheckBvNameClashes(Absy! absy, string! name) {
+ 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)
+ {
+ assert (td is TypeCtorDecl) || (td is TypeSynonymDecl);
+
+ string! name = (!)td.Name;
+ if (CheckBvNameClashes(td, name))
+ return; // error has already been reported
+
+ if (types[name] != null)
+ {
+ Error(td, "more than one declaration of type name: {0}", name);
+ }
+ else
+ {
+ types.Add(name, td);
+ }
+ }
+
+ /// <summary>
+ /// 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
+ /// </summary>
+ /// <param name="name"></param>
+ /// <returns></returns>
+ public TypeCtorDecl LookUpType(string! name)
+ {
+ return types[name] as TypeCtorDecl;
+ }
+
+ public TypeSynonymDecl LookUpTypeSynonym(string! name)
+ {
+ return types[name] as TypeSynonymDecl;
+ }
+
+ // ------------------------------ Boogie 2 Type Binders ------------------------------
+
+ List<TypeVariable!>! typeBinders = new List<TypeVariable!>(5);
+
+ public void AddTypeBinder(TypeVariable! td) {
+ 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); }
+ }
+
+ /// <summary>
+ /// Returns the declaration of the named type binder, or null if
+ /// no such binder is declared.
+ /// </summary>
+ public TypeVariable LookUpTypeBinder(string! name)
+ {
+ for (int i = typeBinders.Count; 0 <= --i; ) {
+ TypeVariable! td = typeBinders[i];
+ if (td.Name == name) {
+ return td;
+ }
+ }
+ return null; // not present
+ }
+
+ // ------------------------------ Types ------------------------------
+
+ // user-defined types
+ // Hashtable /*string->TypeDecl*/! types = new Hashtable /*string->TypeDecl*/ ();
+/*
+ public void AddType(TypeDecl! td)
+ {
+ string! name = (!)td.Name;
+
+ if (name.StartsWith("bv") && name.Length > 2) {
+ bool isBv = true;
+ for (int i = 2; i < name.Length; ++i)
+ if (!char.IsDigit(name[i])) isBv = false;
+ if (isBv)
+ Error(td, "type name: {0} is registered for bitvectors", name);
+ }
+
+ if (types[name] != null)
+ {
+ Error(td, "more than one declaration of type name: {0}", name);
+ }
+ else
+ {
+ types.Add(name, td);
+ }
+ }
+*/
+ /// <summary>
+ /// Returns the declaration of the named type, or null if
+ /// no such type is declared.
+ /// </summary>
+ /// <param name="name"></param>
+ /// <returns></returns>
+ /* public TypeDecl LookUpType(string! name)
+ {
+ return (TypeDecl)types[name];
+ }
+ */
+ // ------------------------------ Type Binders ------------------------------
+/*
+ List<TypeBinderDecl!>! typeBinders = new List<TypeBinderDecl!>(5);
+
+ public void AddTypeBinder(TypeBinderDecl! td) {
+ for (int i = 0; i < typeBinders.Count; i++) {
+ if (typeBinders[i].Name == td.Name) {
+ Error(td, "more than one declaration of type binder name: {0}", td.Name);
+ return;
+ }
+ }
+ typeBinders.Add(td);
+ }
+
+ public int TypeBinderState {
+ get { return typeBinders.Count; }
+ set { typeBinders.RemoveRange(value, typeBinders.Count - value); }
+ }
+
+ /// <summary>
+ /// Returns the declaration of the named type binder, or null if
+ /// no such binder is declared.
+ /// </summary>
+ public TypeDecl LookUpTypeBinder(string! name)
+ {
+ for (int i = typeBinders.Count; 0 <= --i; ) {
+ TypeBinderDecl td = typeBinders[i];
+ if (td.Name == name) {
+ return td;
+ }
+ }
+ return null; // not present
+ }
+ */
+ // ------------------------------ Variables ------------------------------
+
+ class VarContextNode
+ {
+ public readonly Hashtable /*string->Variable*/! VarSymbols = new Hashtable /*string->Variable*/();
+ public /*maybe null*/ VarContextNode ParentContext;
+ public readonly bool Opaque;
+
+ 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);
+
+ /// <summary>
+ /// Adds a variable context.
+ /// </summary>
+ public void PushVarContext()
+ {
+ varContext = new VarContextNode(varContext, false);
+ }
+
+ /// <summary>
+ /// Adds an opaque variable context, that is, one that blocks all previously pushed contexts.
+ /// </summary>
+ public void PushOpaqueVarContext()
+ {
+ varContext = new VarContextNode(varContext, true);
+ }
+
+ /// <summary>
+ /// Requires there to be more than one variable context.
+ /// </summary>
+ public void PopVarContext()
+ {
+ assert varContext.ParentContext != null;
+ varContext = varContext.ParentContext;
+ }
+
+ public void AddVariable(Variable! var, bool global)
+ {
+ if (FindVariable((!)var.Name, !global) != null)
+ {
+ Error(var, "more than one declaration of variable name: {0}", var.Name);
+ }
+ else
+ {
+ varContext.VarSymbols.Add(var.Name, var);
+ }
+ }
+
+ /// <summary>
+ /// Returns the declaration of the named variable, or null if
+ /// no such variable is declared.
+ /// </summary>
+ /// <param name="name"></param>
+ /// <returns></returns>
+ public Variable LookUpVariable(string! name)
+ {
+ return FindVariable(name, false);
+ }
+
+ Variable FindVariable(string! name, bool ignoreTopLevelVars)
+ {
+ 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;
+ }
+
+ // ------------------------------ Functions/Procedures ------------------------------
+
+ // uninterpreted function symbols, procedures
+ Hashtable /*string->DeclWithFormals*/! funcdures = new Hashtable /*string->DeclWithFormals*/ ();
+
+ public void AddProcedure(DeclWithFormals! proc)
+ {
+ if (funcdures[(!)proc.Name] != null)
+ {
+ Error(proc, "more than one declaration of function/procedure name: {0}", proc.Name);
+ }
+ else
+ {
+ funcdures.Add(proc.Name, proc);
+ }
+ }
+
+ /// <summary>
+ /// Returns the declaration of the named function/procedure, or null if
+ /// no such function or procedure is declared.
+ /// </summary>
+ /// <param name="name"></param>
+ /// <returns></returns>
+ public DeclWithFormals LookUpProcedure(string! name)
+ {
+ return (DeclWithFormals)funcdures[name];
+ }
+
+ // ------------------------------ Blocks ------------------------------
+
+ class ProcedureContext {
+ 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; }
+ }
+
+ /// <summary>
+ /// Pushes a new procedure context.
+ /// </summary>
+ public void PushProcedureContext()
+ ensures HasProcedureContext;
+ {
+ procedureContext = new ProcedureContext(procedureContext);
+ }
+
+ /// <summary>
+ /// Requires there to be a procedure context. Pops it.
+ /// </summary>
+ public void PopProcedureContext()
+ requires HasProcedureContext;
+ {
+ assert procedureContext != null; // follows from precondition
+ procedureContext = procedureContext.Next;
+ }
+
+ /// <summary>
+ /// Requires there to be a procedure context.
+ /// </summary>
+ /// <param name="block"></param>
+ public void AddBlock(Block! block)
+ requires HasProcedureContext;
+ {
+ assert procedureContext != null; // follows from precondition
+ Hashtable! /*string->Block!*/ blocks = procedureContext.Blocks;
+ if (blocks[block.Label] != null)
+ {
+ Error(block, "more than one declaration of block name: {0}", block.Label);
+ }
+ else
+ {
+ blocks.Add(block.Label, block);
+ }
+ }
+
+ /// <summary>
+ /// Requires there to be a procedure context.
+ /// Returns the declaration of the named block, or null if
+ /// no such block is declared.
+ /// </summary>
+ /// <param name="name"></param>
+ /// <returns></returns>
+ public Block LookUpBlock(string! name)
+ requires HasProcedureContext;
+ {
+ assert procedureContext != null; // follows from precondition
+ Hashtable! /*string->Block!*/ blocks = procedureContext.Blocks;
+ return (Block)blocks[name];
+ }
+
+ // ------------------------------ Flags ------------------------------
+
+ public enum State { StateLess, Single, Two }
+ State stateMode = State.Single;
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ public State StateMode {
+ get {
+ return stateMode;
+ }
+ set {
+ assert value != stateMode;
+ assert stateMode == State.Single || value == State.Single;
+ expose (this) {
+ stateMode = value;
+ }
+ }
+ }
+
+ bool triggerMode = false;
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ public bool TriggerMode
+ {
+ get
+ {
+ return triggerMode;
+ }
+ set
+ {
+ assert triggerMode != value;
+ expose (this) {
+ triggerMode = value;
+ }
+ }
+ }
+ }
+
+ public class TypecheckingContext : CheckingContext
+ {
+ public IdentifierExprSeq Frame; // used in checking the assignment targets of implementation bodies
+
+ public TypecheckingContext(IErrorSink errorSink)
+ {
+ base(errorSink);
+ }
+
+ public bool InFrame(Variable! v)
+ requires Frame != null;
+ {
+ return exists{IdentifierExpr! ie in Frame; ie.Decl == v};
+ }
+ }
+}
|