Merge branch 'master' into aggressive_chop

build.sbt

@@ -34,7 +34,8 @@ lazy val gobra = (project in file("."))
     libraryDependencies += "org.apache.commons" % "commons-lang3" % "3.9", // for SystemUtils
     libraryDependencies += "org.apache.commons" % "commons-text" % "1.9", // for escaping strings in parser preprocessor
     libraryDependencies += "commons-codec" % "commons-codec" % "1.15", // for obtaining the hex encoding of a string
-    libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.9.2",
+    libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.13.0",
+    libraryDependencies += "org.scalaz" %% "scalaz-core" % "7.3.7", // used for EitherT
 
     scalacOptions ++= Seq(
       "-encoding", "UTF-8", // Enforce UTF-8, instead of relying on properly set locales

src/main/antlr4/GoLexer.g4

@@ -34,8 +34,7 @@
  * https://golang.org/ref/spec
  */
 
-// Imported to Gobra from https://github.com/antlr/grammars-v4/blob/4c06ad8cc8130931c75ca0b17cbc1453f3830cd2/golang
-
+// Imported to Gobra from https://github.com/antlr/grammars-v4/blob/fae6a8500e9c6a1ec895fca1495b0384b9144091/golang
 
 lexer grammar GoLexer;
 
@@ -145,7 +144,7 @@ HEX_FLOAT_LIT          : '0' [xX] HEX_MANTISSA HEX_EXPONENT
 fragment HEX_MANTISSA  : ('_'? HEX_DIGIT)+ ('.' ( '_'? HEX_DIGIT )*)?
                        | '.' HEX_DIGIT ('_'? HEX_DIGIT)*;
 
-fragment HEX_EXPONENT  : [pP] [+-] DECIMALS;
+fragment HEX_EXPONENT  : [pP] [+-]? DECIMALS;
 
 
 IMAGINARY_LIT          : (DECIMAL_LIT | BINARY_LIT |  OCTAL_LIT | HEX_LIT | FLOAT_LIT) 'i' -> mode(NLSEMI);
@@ -172,42 +171,54 @@ BIG_U_VALUE: '\\' 'U' HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGI
 
 RAW_STRING_LIT         : '`' ~'`'*                      '`' -> mode(NLSEMI);
 INTERPRETED_STRING_LIT : '"' (~["\\] | ESCAPED_VALUE)*  '"' -> mode(NLSEMI);
+
 // Hidden tokens
+
 WS                     : [ \t]+             -> channel(HIDDEN);
 COMMENT                : '/*' .*? '*/'      -> channel(HIDDEN);
 TERMINATOR             : [\r\n]+            -> channel(HIDDEN);
 LINE_COMMENT           : '//' ~[\r\n]*      -> channel(HIDDEN);
 
 fragment UNICODE_VALUE: ~[\r\n'] | LITTLE_U_VALUE | BIG_U_VALUE | ESCAPED_VALUE;
+
 // Fragments
+
 fragment ESCAPED_VALUE
     : '\\' ('u' HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT
            | 'U' HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT
            | [abfnrtv\\'"]
            | OCTAL_DIGIT OCTAL_DIGIT OCTAL_DIGIT
            | 'x' HEX_DIGIT HEX_DIGIT)
     ;
+
 fragment DECIMALS
     : [0-9] ('_'? [0-9])*
     ;
+
 fragment OCTAL_DIGIT
     : [0-7]
     ;
+
 fragment HEX_DIGIT
     : [0-9a-fA-F]
     ;
+
 fragment BIN_DIGIT
     : [01]
     ;
+
 fragment EXPONENT
     : [eE] [+-]? DECIMALS
     ;
+
 fragment LETTER
     : UNICODE_LETTER
     | '_'
     ;
+
 fragment UNICODE_DIGIT
     : [\p{Nd}]
+
     /*  [\u0030-\u0039]
     | [\u0660-\u0669]
     | [\u06F0-\u06F9]
@@ -229,6 +240,7 @@ fragment UNICODE_DIGIT
     | [\u1810-\u1819]
     | [\uFF10-\uFF19]*/
     ;
+
 fragment UNICODE_LETTER
     : [\p{L}]
     /*  [\u0041-\u005A]
@@ -494,7 +506,11 @@ fragment UNICODE_LETTER
     | [\uFFDA-\uFFDC]
     */
     ;
+
+
 mode NLSEMI;
+
+
 // Treat whitespace as normal
 WS_NLSEMI                     : [ \t]+             -> channel(HIDDEN);
 // Ignore any comments that only span one line
@@ -504,4 +520,4 @@ LINE_COMMENT_NLSEMI : '//' ~[\r\n]*      -> channel(HIDDEN);
 //return to normal lexing
 EOS:              ([\r\n]+ | ';' | '/*' .*? '*/' | EOF)            -> mode(DEFAULT_MODE);
 // Did not find an EOS, so go back to normal lexing
-OTHER: -> mode(DEFAULT_MODE), channel(HIDDEN);
+OTHER: -> mode(DEFAULT_MODE), channel(HIDDEN);

src/main/antlr4/GoParser.g4

@@ -28,11 +28,12 @@
  (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
  THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
+
 /*
  * A Go grammar for ANTLR 4 derived from the Go Language Specification https://golang.org/ref/spec
  */
 
-// Imported to Gobra from https://github.com/antlr/grammars-v4/blob/4c06ad8cc8130931c75ca0b17cbc1453f3830cd2/golang
+// Imported to Gobra from https://github.com/antlr/grammars-v4/tree/fae6a8500e9c6a1ec895fca1495b0384b9144091/golang
 
 parser grammar GoParser;
 
@@ -87,7 +88,7 @@ varSpec:
 
 block: L_CURLY statementList? R_CURLY;
 
-statementList: (eos? statement eos)+;
+statementList: ((SEMI? | EOS? | {this.closingBracket()}?) statement eos)+;
 
 statement:
 	declaration
@@ -194,7 +195,7 @@ commCase: CASE (sendStmt | recvStmt) | DEFAULT;
 
 recvStmt: (expressionList ASSIGN | identifierList DECLARE_ASSIGN)? recvExpr = expression;
 
-forStmt: FOR (expression | forClause | rangeClause)? block;
+forStmt: FOR (expression? | forClause | rangeClause?) block;
 
 forClause:
 	initStmt = simpleStmt? eos expression? eos postStmt = simpleStmt?;
@@ -384,5 +385,5 @@ eos:
 	SEMI
 	| EOF
 	| EOS
-	| {closingBracket()}?
-	;
+	| {this.closingBracket()}?
+	;

src/main/antlr4/GobraParser.g4

@@ -39,6 +39,10 @@ sourceFile:
     (specMember | declaration | ghostMember) eos
   )* EOF;
 
+// `preamble` is a second entry point allowing us to parse only the top of a source.
+// That's also why we don not enforce EOF at the end.
+preamble: (initPost eos)* packageClause eos (importDecl eos)*;
+
 initPost: INIT_POST expression;
 
 importPre: IMPORT_PRE expression;
@@ -146,7 +150,9 @@ domainClause: FUNC IDENTIFIER signature | AXIOM L_CURLY expression eos R_CURLY;
 
 adtType: ADT L_CURLY (adtClause eos)* R_CURLY;
 
-adtClause: IDENTIFIER L_CURLY (fieldDecl eos)* R_CURLY;
+adtClause: IDENTIFIER L_CURLY (adtFieldDecl eos)* R_CURLY;
+
+adtFieldDecl: identifierList? type_;
 
 ghostSliceType: GHOST L_BRACKET R_BRACKET elementType;