From a3d7bd9b4a7b62cb0d8e4b0762d8db51c1548f1e Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 13 May 2011 14:38:28 -0700 Subject: Boogie: added features to help with modular verification. In particular, define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations. --- Source/Core/Absy.cs | 26 +++---- Source/Core/CommandLineOptions.cs | 15 ++++ Source/Core/ResolutionContext.cs | 142 ++++++++++++++++---------------------- 3 files changed, 85 insertions(+), 98 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index cde8fc3f..67500c88 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -235,30 +235,26 @@ namespace Microsoft.Boogie { ResolveTypes(rc); - List prunedTopLevelDecls = CommandLineOptions.Clo.OverlookBoogieTypeErrors ? new List() : null; - + var prunedTopLevelDecls = new List(); foreach (Declaration d in TopLevelDeclarations) { + if (QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) { + continue; + } // resolve all the non-type-declarations if (d is TypeCtorDecl || d is TypeSynonymDecl) { - if (prunedTopLevelDecls != null) - prunedTopLevelDecls.Add(d); } else { int e = rc.ErrorCount; d.Resolve(rc); - if (prunedTopLevelDecls != null) { - if (rc.ErrorCount != e && d is Implementation) { - // ignore this implementation - System.Console.WriteLine("Warning: Ignoring implementation {0} because of translation resolution errors", ((Implementation)d).Name); - rc.ErrorCount = e; - } else { - prunedTopLevelDecls.Add(d); - } + if (CommandLineOptions.Clo.OverlookBoogieTypeErrors && rc.ErrorCount != e && d is Implementation) { + // ignore this implementation + System.Console.WriteLine("Warning: Ignoring implementation {0} because of translation resolution errors", ((Implementation)d).Name); + rc.ErrorCount = e; + continue; } } + prunedTopLevelDecls.Add(d); } - if (prunedTopLevelDecls != null) { - TopLevelDeclarations = prunedTopLevelDecls; - } + TopLevelDeclarations = prunedTopLevelDecls; foreach (Declaration d in TopLevelDeclarations) { Variable v = d as Variable; diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 5094fb9e..84ecce6d 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1875,6 +1875,21 @@ namespace Microsoft.Boogie { Console.WriteLine( @"Boogie: The following attributes are supported by this implementation. + ---- On top-level declarations --------------------------------------------- + + {:ignore} + Ignore the declaration (after checking for duplicate names). + See also below for more options when :ignore is used with axioms. + + {:extern} + If two top-level declarations introduce the same name (for example, two + constants with the same name or two procedures with the same name), then + Boogie usually produces an error message. However, if at least one of + the declarations is declared with :extern, one of the declarations is + ignored. If both declarations are :extern, Boogie arbitrarily chooses + one of them to keep; otherwise, Boogie ignore the :extern declaration + and keeps the other. + ---- On axioms ------------------------------------------------------------- {:inline true} diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index d4b353ef..803b1f8b 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -170,15 +170,22 @@ namespace Microsoft.Boogie { public void AddType(NamedDeclaration td) { Contract.Requires(td != null); Contract.Assert((td is TypeCtorDecl) || (td is TypeSynonymDecl)); + Contract.Requires(td.Name != null); - string name = cce.NonNull(td.Name); + 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 { + 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; + } } } @@ -247,79 +254,6 @@ namespace Microsoft.Boogie { return null; // not present } - // ------------------------------ Types ------------------------------ - - // user-defined types - // Hashtable /*string->TypeDecl*/! types = new Hashtable /*string->TypeDecl*/ (); - /* - public void AddType(TypeDecl td){ - Contract.Requires(td != null); - 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); - } - } - */ - /// - /// Returns the declaration of the named type, or null if - /// no such type is declared. - /// - /// - /// - /* public TypeDecl LookUpType(string name){ -Contract.Requires(name != null); - return (TypeDecl)types[name]; - } - */ - // ------------------------------ Type Binders ------------------------------ - /* - List! typeBinders = new List(5); - - public void AddTypeBinder(TypeBinderDecl td){ - Contract.Requires(td != null); - 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); } - } - - /// - /// Returns the declaration of the named type binder, or null if - /// no such binder is declared. - /// - public TypeDecl LookUpTypeBinder(string name){ - Contract.Requires(name != null); - for (int i = typeBinders.Count; 0 <= --i; ) { - TypeBinderDecl td = typeBinders[i]; - if (td.Name == name) { - return td; - } - } - return null; // not present - } - */ // ------------------------------ Variables ------------------------------ class VarContextNode { @@ -365,10 +299,16 @@ Contract.Requires(name != null); public void AddVariable(Variable var, bool global) { Contract.Requires(var != null); - if (FindVariable(cce.NonNull(var.Name), !global) != null) { - Error(var, "more than one declaration of variable name: {0}", var.Name); - } else { + 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; + } } } @@ -417,11 +357,47 @@ Contract.Requires(name != null); public void AddProcedure(DeclWithFormals proc) { Contract.Requires(proc != null); - if (funcdures[cce.NonNull(proc.Name)] != null) { - Error(proc, "more than one declaration of function/procedure name: {0}", proc.Name); + 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 { - funcdures.Add(proc.Name, proc); + return null; } + // prepend :ignore attribute + ignore.Attributes = new QKeyValue(ignore.tok, "ignore", new List(), ignore.Attributes); + return keep; } /// -- cgit v1.2.3