Report errors originating from included files when verifying includin…

…g file

Closes #16

Source/Dafny/DafnyAst.cs

@@ -85,12 +85,14 @@ public class Include : IComparable
  public readonly string includerFilename;
  public readonly string includedFilename;
  public readonly string includedFullPath;
+ public bool ErrorReported;
 
  public Include(IToken tok, string includer, string theFilename, string fullPath) {
  this.tok = tok;
  this.includerFilename = includer;
  this.includedFilename = theFilename;
  this.includedFullPath = fullPath;
+ this.ErrorReported = false;
  }
 
  public int CompareTo(object obj) {
@@ -6755,7 +6757,7 @@ public int pos {
  get { return WrappedToken.pos; }
  set { throw new NotSupportedException(); }
  }
- public string val {
+ public virtual string val {
  get { return WrappedToken.val; }
  set { throw new NotSupportedException(); }
  }
@@ -6781,9 +6783,16 @@ public NestedToken(IToken outer, IToken inner)
  /// </summary>
  public class IncludeToken : TokenWrapper
  {
- public IncludeToken(IToken wrappedToken)
+ public Include Include;
+ public IncludeToken(Include include, IToken wrappedToken)
  : base(wrappedToken) {
  Contract.Requires(wrappedToken != null);
+ this.Include = include;
+ }
+
+ public override string val {
+ get { return WrappedToken.val; }
+ set { WrappedToken.val = value; }
  }
  }
 

Source/Dafny/DafnyMain.cs

@@ -113,7 +113,7 @@ public static string Parse(IList<DafnyFile> files, string programName, ErrorRepo
  Console.WriteLine("Parsing " + dafnyFile.FilePath);
  }
 
- string err = ParseFile(dafnyFile, Bpl.Token.NoToken, module, builtIns, new Errors(reporter));
+ string err = ParseFile(dafnyFile, null, module, builtIns, new Errors(reporter));
  if (err != null) {
  return err;
  }
@@ -188,7 +188,7 @@ public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, IList<s
  catch (IllegalDafnyFile){
  return (String.Format("Include of file \"{0}\" failed.", include.includedFilename));
  }
- string ret = ParseFile(file, include.tok, module, builtIns, errs, false);
+ string ret = ParseFile(file, include, module, builtIns, errs, false);
  if (ret != null) {
  return ret;
  }
@@ -203,14 +203,15 @@ public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, IList<s
  return null; // Success
  }
 
- private static string ParseFile(DafnyFile dafnyFile, Bpl.IToken tok, ModuleDecl module, BuiltIns builtIns, Errors errs, bool verifyThisFile = true) {
+ private static string ParseFile(DafnyFile dafnyFile, Include include, ModuleDecl module, BuiltIns builtIns, Errors errs, bool verifyThisFile = true) {
  var fn = DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath;
  try {
- int errorCount = Dafny.Parser.Parse(dafnyFile.SourceFileName, module, builtIns, errs, verifyThisFile);
+ int errorCount = Dafny.Parser.Parse(dafnyFile.SourceFileName, include, module, builtIns, errs, verifyThisFile);
  if (errorCount != 0) {
  return string.Format("{0} parse errors detected in {1}", errorCount, fn);
  }
  } catch (IOException e) {
+ Bpl.IToken tok = include == null ? Bpl.Token.NoToken : include.tok; 
  errs.SemErr(tok, "Unable to open included file");
  return string.Format("Error opening file \"{0}\": {1}", fn, e.Message);
  }

Source/Dafny/Parser.cs

@@ -87,14 +87,15 @@ public class Parser {
  public Scanner scanner;
  public Errors errors;
 
- public Token t; // last recognized token
- public Token la; // lookahead token
+ public IToken t; // last recognized token
+ public IToken la; // lookahead token
  int errDist = minErrDist;
 
 readonly Expression/*!*/ dummyExpr;
 readonly AssignmentRhs/*!*/ dummyRhs;
 readonly FrameExpression/*!*/ dummyFrameExpr; 
 readonly Statement/*!*/ dummyStmt;
+readonly Include theInclude;
 readonly ModuleDecl theModule;
 readonly BuiltIns theBuiltIns;
 readonly bool theVerifyThisFile;
@@ -215,17 +216,17 @@ static void EncodeExternAsAttribute(DeclModifierData dmod, ref Attributes attrs,
 /// Returns the number of parsing errors encountered.
 /// Note: first initialize the Scanner.
 ///</summary>
-public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ {
+public static int Parse (string/*!*/ filename, Include include, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ {
  Contract.Requires(filename != null);
  Contract.Requires(module != null);
  string s;
  if (filename == "stdin.dfy") {
  s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());
- return Parse(s, filename, filename, module, builtIns, errors, verifyThisFile);
+ return Parse(s, filename, filename, include, module, builtIns, errors, verifyThisFile);
  } else {
  using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
  s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());
- return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);
+ return Parse(s, filename, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, include, module, builtIns, errors, verifyThisFile);
  }
  }
 }
@@ -240,15 +241,15 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi
  Contract.Requires(filename != null);
  Contract.Requires(module != null);
  Errors errors = new Errors(reporter);
- return Parse(s, fullFilename, filename, module, builtIns, errors, verifyThisFile);
+ return Parse(s, fullFilename, filename, null, module, builtIns, errors, verifyThisFile);
 }
 ///<summary>
 /// Parses top-level things (modules, classes, datatypes, class members)
 /// and appends them in appropriate form to "module".
 /// Returns the number of parsing errors encountered.
 /// Note: first initialize the Scanner with the given Errors sink.
 ///</summary>
-public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, ModuleDecl module,
+public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ filename, Include include, ModuleDecl module,
  BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) {
  Contract.Requires(s != null);
  Contract.Requires(filename != null);
@@ -257,18 +258,19 @@ public static int Parse (string/*!*/ s, string/*!*/ fullFilename, string/*!*/ fi
  byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
  MemoryStream ms = new MemoryStream(buffer,false);
  Scanner scanner = new Scanner(ms, errors, fullFilename, filename);
- Parser parser = new Parser(scanner, errors, module, builtIns, verifyThisFile);
+ Parser parser = new Parser(scanner, errors, include, module, builtIns, verifyThisFile);
  parser.Parse();
  return parser.errors.ErrorCount;
 }
-public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
+public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, Include include, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
  : this(scanner, errors) // the real work
 {
  // initialize readonly fields
  dummyExpr = new LiteralExpr(Token.NoToken);
  dummyRhs = new ExprRhs(dummyExpr, null);
  dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
  dummyStmt = new ReturnStmt(Token.NoToken, Token.NoToken, null);
+ theInclude = include; // the "include" that includes this file
  theModule = module;
  theBuiltIns = builtIns;
  theVerifyThisFile = verifyThisFile;
@@ -679,7 +681,7 @@ public void SemErr(IToken tok, string msg) {
 
  void Get () {
  for (;;) {
- t = la;
+ t = theVerifyThisFile ? la : new IncludeToken(theInclude, la);
  la = scanner.Scan();
  if (la.kind <= maxT) { ++errDist; break; }
 
@@ -1089,10 +1091,10 @@ void NewtypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDec
  if (baseType == null) { baseType = new InferredTypeProxy(); } 
  Expect(24);
  Expression(out wh, false, true);
- td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); 
+ td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); 
  } else if (StartOf(6)) {
  Type(out baseType);
- td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); 
+ td = new NewtypeDecl(id, id.val, module, baseType, attrs); 
  } else SynErr(161);
  }
 
@@ -1134,7 +1136,7 @@ void OtherTypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelD
  if (ty == null) { ty = new InferredTypeProxy(); } 
  Expect(24);
  Expression(out constraint, false, true);
- td = new SubsetTypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs);
+ td = new SubsetTypeDecl(id, id.val, typeArgs, module, new BoundVar(bvId, bvId.val, ty), constraint, attrs);
  kind = "Subset type";
 
  } else if (StartOf(6)) {
@@ -1665,7 +1667,7 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi
  SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");
  }
  EncodeExternAsAttribute(dmod, ref attrs, id, /* needAxiom */ true);
- IToken tok = theVerifyThisFile ? id : new IncludeToken(id);
+ IToken tok = id;
  if (isTwoState && isPredicate) {
  f = new TwoStatePredicate(tok, id.val, dmod.IsStatic, typeArgs, formals,
  reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureEllipsis);
@@ -1824,8 +1826,8 @@ void MethodDecl(DeclModifierData dmod, bool allowConstructor, bool isWithinAbstr
  if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {
  SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");
  }
- 
- IToken tok = theVerifyThisFile ? id : new IncludeToken(id);
+
+ IToken tok = id;
  if (isConstructor) {
  m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,
  req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
@@ -2990,7 +2992,7 @@ void WhileStmt(out Statement stmt) {
 
  void MatchStmt(out Statement/*!*/ s) {
  Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
+ IToken x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
  List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
  bool usesOptionalBraces = false;
 
@@ -3080,7 +3082,7 @@ void ForallStmt(out Statement/*!*/ s) {
 
  void CalcStmt(out Statement s) {
  Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- Token x;
+ IToken x;
  Attributes attrs = null;
  CalcStmt.CalcOp op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
  var lines = new List<Expression>();

Source/Dafny/Reporting.cs

@@ -37,7 +37,7 @@ protected ErrorReporter() {
  // This is the only thing that needs to be overriden
  public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {
  bool discard = (ErrorsOnly && level != ErrorLevel.Error) || // Discard non-errors if ErrorsOnly is set
- (tok is TokenWrapper && !(tok is NestedToken) && !(tok is RefinementToken)); // Discard wrapped tokens, except for nested and refinement
+ (tok is TokenWrapper && !(tok is IncludeToken) && !(tok is NestedToken) && !(tok is RefinementToken)); // Discard wrapped tokens, except for included, nested and refinement
  if (!discard) {
  AllMessages[level].Add(new ErrorMessage { token = tok, message = msg });
  }
@@ -51,6 +51,16 @@ public int Count(ErrorLevel level) {
  public void Error(MessageSource source, IToken tok, string msg) {
  Contract.Requires(tok != null);
  Contract.Requires(msg != null);
+ // if the tok is IncludeToken, we need to indicate to the including file
+ // that there are errors in the included file.
+ if (tok is IncludeToken) {
+ IncludeToken includeToken = (IncludeToken) tok;
+ Include include = includeToken.Include;
+ if (!include.ErrorReported) {
+ Message(source, ErrorLevel.Error, include.tok, "the included file " + tok.filename + " contains error(s)");
+ include.ErrorReported = true;
+ }
+ }
  Message(source, ErrorLevel.Error, tok, msg);
  }
 

Source/DafnyServer/DafnyHelper.cs

@@ -50,7 +50,7 @@ public bool Verify() {
  private bool Parse() {
  Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);
  Dafny.BuiltIns builtIns = new Dafny.BuiltIns();
- var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, new Dafny.Errors(reporter)) == 0 &&
+ var success = (Dafny.Parser.Parse(source, fname, fname, null, module, builtIns, new Dafny.Errors(reporter)) == 0 &&
  Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), new Dafny.Errors(reporter)) == null);
  if (success) {
  dafnyProgram = new Dafny.Program(fname, module, builtIns, reporter);

Test/allocated1/dafny0/AssumptionVariables0.dfy.expect

@@ -1,3 +1,4 @@
+AssumptionVariables0.dfy(3,8): Error: the included file AssumptionVariables0.dfy contains error(s)
 AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
 AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && <boolean expression>"
 AssumptionVariables0.dfy(9,26): Error: assumption variable must be of type 'bool'
@@ -10,4 +11,4 @@ AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to a
 AssumptionVariables0.dfy(61,34): Error: assumption variable must be of type 'bool'
 AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
 AssumptionVariables0.dfy(78,20): Error: assumption variable must be ghost
-12 resolution/type errors detected in AssumptionVariables0.dfy
+13 resolution/type errors detected in AssumptionVariables0.dfy

Test/allocated1/dafny0/BindingGuardsResolution.dfy.expect

@@ -154,6 +154,7 @@ module Ghost {
  b := exists y {:myattribute P(y)} :: 0 <= y < 100;
  }
 }
+BindingGuardsResolution.dfy(3,8): Error: the included file BindingGuardsResolution.dfy contains error(s)
 BindingGuardsResolution.dfy(12,10): Error: Duplicate local-variable name: x
 BindingGuardsResolution.dfy(19,6): Error: LHS of assignment must denote a mutable variable
 BindingGuardsResolution.dfy(39,8): Error: Duplicate local-variable name: x
@@ -165,4 +166,4 @@ BindingGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is n
 BindingGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
 BindingGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
 BindingGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-11 resolution/type errors detected in BindingGuardsResolution.dfy
+12 resolution/type errors detected in BindingGuardsResolution.dfy

Test/allocated1/dafny0/BitvectorResolution.dfy.expect

@@ -1,3 +1,4 @@
+BitvectorResolution.dfy(3,8): Error: the included file BitvectorResolution.dfy contains error(s)
 BitvectorResolution.dfy(9,13): Error: bitvector literal (5000) is too large for the type bv1
 BitvectorResolution.dfy(15,9): Error: bitvector literal (1) is too large for the type bv0
 BitvectorResolution.dfy(18,9): Error: bitvector literal (4294967296) is too large for the type bv32
@@ -11,4 +12,4 @@ BitvectorResolution.dfy(43,26): Error: type mismatch for argument 0 (function ex
 BitvectorResolution.dfy(40,15): Error: type of right argument to << (real) must be an integer-numeric or bitvector type
 BitvectorResolution.dfy(41,15): Error: type of right argument to << (SmallReal) must be an integer-numeric or bitvector type
 BitvectorResolution.dfy(110,19): Error: the type of this expression is underspecified
-13 resolution/type errors detected in BitvectorResolution.dfy
+14 resolution/type errors detected in BitvectorResolution.dfy

Test/allocated1/dafny0/CallStmtTests.dfy.expect

@@ -1,3 +1,4 @@
+CallStmtTests.dfy(3,8): Error: the included file CallStmtTests.dfy contains error(s)
 CallStmtTests.dfy(7,4): Error: LHS of assignment must denote a mutable variable
 CallStmtTests.dfy(20,11): Error: actual out-parameter 0 is required to be a ghost variable
-2 resolution/type errors detected in CallStmtTests.dfy
+3 resolution/type errors detected in CallStmtTests.dfy

Test/allocated1/dafny0/CoResolution.dfy.expect

@@ -1,3 +1,4 @@
+CoResolution.dfy(3,8): Error: the included file CoResolution.dfy contains error(s)
 CoResolution.dfy(18,11): Error: member Undeclared# does not exist in class TestClass
 CoResolution.dfy(19,6): Error: unresolved identifier: Undeclared#
 CoResolution.dfy(22,9): Error: unresolved identifier: _k
@@ -23,4 +24,4 @@ CoResolution.dfy(206,12): Error: type variable '_T0' in the function call to 'A'
 CoResolution.dfy(206,13): Error: the type of this expression is underspecified
 CoResolution.dfy(206,19): Error: type variable '_T0' in the function call to 'S' could not be determined
 CoResolution.dfy(206,20): Error: the type of this expression is underspecified
-25 resolution/type errors detected in CoResolution.dfy
+26 resolution/type errors detected in CoResolution.dfy

Test/allocated1/dafny0/Coinductive.dfy.expect

@@ -1,3 +1,4 @@
+Coinductive.dfy(3,8): Error: the included file Coinductive.dfy contains error(s)
 Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
 Coinductive.dfy(16,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
 Coinductive.dfy(38,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
@@ -28,4 +29,4 @@ Coinductive.dfy(253,12): Error: an inductive predicate can be called recursively
 Coinductive.dfy(259,15): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
 Coinductive.dfy(260,10): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
 Coinductive.dfy(280,21): Error: a recursive call from an inductive predicate can go only to other inductive predicates
-30 resolution/type errors detected in Coinductive.dfy
+31 resolution/type errors detected in Coinductive.dfy

Test/allocated1/dafny0/DatatypeUpdateResolution.dfy.expect

@@ -1,5 +1,6 @@
+DatatypeUpdateResolution.dfy(3,8): Error: the included file DatatypeUpdateResolution.dfy contains error(s)
 DatatypeUpdateResolution.dfy(12,22): Error: member 'non_destructor' does not exist in datatype 'MyDataType'
 DatatypeUpdateResolution.dfy(13,38): Error: member '40' does not exist in datatype 'MyDataType'
 DatatypeUpdateResolution.dfy(17,61): Error: duplicate update member 'otherbool'
 DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor ('otherbool' belongs to 'MyOtherConstructor' and '42' belongs to 'MyNumericConstructor'
-4 resolution/type errors detected in DatatypeUpdateResolution.dfy
+5 resolution/type errors detected in DatatypeUpdateResolution.dfy