Skip to content

Commit

Permalink
Squashed commit of the following:
Browse files Browse the repository at this point in the history 
commit caca746
Author: Felix Wolf <60103963+Felalolf@users.noreply.github.com>
Date:   Thu Aug 17 13:38:33 2023 +0200

    Fix viperproject#668 (viperproject#669)

commit f21fe70
Author: viper-admin <59963956+viper-admin@users.noreply.github.com>
Date:   Wed Aug 2 19:46:32 2023 +0200

    Updates submodules (viperproject#667)

    Co-authored-by: ArquintL <ArquintL@users.noreply.github.com>

commit 3590b3c
Merge: 4a27390 04a7a2a
Author: Linard Arquint <ArquintL@users.noreply.github.com>
Date:   Tue Jul 18 16:20:45 2023 +0200

    Merge pull request viperproject#665 from viperproject/avoid-printing-asts

    Avoiding accidental printing of ASTs

commit 04a7a2a
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Jul 18 15:07:32 2023 +0200

    adapts  to avoid accidental printing of ASTs

commit 4a27390
Merge: 8f9bfa7 a132190
Author: Linard Arquint <ArquintL@users.noreply.github.com>
Date:   Tue Jul 18 10:02:56 2023 +0200

    Merge pull request viperproject#634 from viperproject/parallel-type-checking

    Parallelizing Gobra

commit a132190
Merge: 716eeeb 4fc3cc9
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Jul 18 09:23:38 2023 +0200

    Merges remote changes

commit 716eeeb
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Jul 18 09:23:21 2023 +0200

    implements CR suggestions by Felix

commit 4fc3cc9
Author: Linard Arquint <ArquintL@users.noreply.github.com>
Date:   Tue Jul 18 09:06:13 2023 +0200

    Update src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala

    Co-authored-by: Felix Wolf <60103963+Felalolf@users.noreply.github.com>

commit 8f9bfa7
Merge: 400015c 940a4b5
Author: Linard Arquint <ArquintL@users.noreply.github.com>
Date:   Tue Jul 18 08:18:36 2023 +0200

    Merge pull request viperproject#664 from viperproject/auto-update-submodules

    Update Submodules

commit 940a4b5
Author: ArquintL <ArquintL@users.noreply.github.com>
Date:   Mon Jul 17 17:36:04 2023 +0000

    Updates submodules

commit 400015c
Merge: 1894cef 64389b2
Author: Linard Arquint <ArquintL@users.noreply.github.com>
Date:   Thu Jul 13 11:20:49 2023 +0200

    Merge pull request viperproject#663 from viperproject/auto-update-submodules

    Update Submodules

commit 64389b2
Author: ArquintL <ArquintL@users.noreply.github.com>
Date:   Thu Jul 13 07:54:42 2023 +0000

    Updates submodules

commit 1894cef
Author: viper-admin <59963956+viper-admin@users.noreply.github.com>
Date:   Wed Jul 12 06:56:11 2023 +0200

    Updates submodules (viperproject#661)

    Co-authored-by: jcp19 <jcp19@users.noreply.github.com>

commit 6e21fcf
Merge: bb3610b ff48d9c
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Wed Jul 5 16:22:22 2023 +0200

    Merges branch 'master' into 'parallel-type-checking'

commit ff48d9c
Merge: c56b335 d34ca31
Author: Linard Arquint <ArquintL@users.noreply.github.com>
Date:   Wed Jul 5 16:08:57 2023 +0200

    Merge pull request viperproject#660 from viperproject/659-quantified-let-expressions-in-encoding-unsoundness

    Fix viperproject#659

commit d34ca31
Merge: 1929662 c56b335
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Wed Jul 5 15:33:11 2023 +0200

    Merges branch 'master' into '659-quantified-let-expressions-in-encoding-unsoundness'

commit c56b335
Merge: 4393ad0 fc634a4
Author: Linard Arquint <ArquintL@users.noreply.github.com>
Date:   Wed Jul 5 15:32:22 2023 +0200

    Merge pull request viperproject#658 from viperproject/auto-update-submodules

    Update Submodules

commit 1929662
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Jul 4 09:30:59 2023 +0200

    updates ViperServer to latest commit

commit 3e87a6a
Merge: 0fdf73a fc634a4
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Jul 4 08:58:25 2023 +0200

    Merges branch 'auto-update-submodules' into '659-quantified-let-expressions-in-encoding-unsoundness'

commit 0fdf73a
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Jul 4 08:57:32 2023 +0200

    adds failing test case

commit fc634a4
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Mon Jul 3 12:19:32 2023 +0200

    fixes a compiler error caused by recent error reporting improvements

commit d64f56a
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Mon Jul 3 12:05:30 2023 +0200

    adapts regression tests to latest Viper changes

commit 9772277
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Mon Jul 3 12:03:33 2023 +0200

    improves reporting of consistency errors and errors resulting from applying Viper transformers

commit 08bfba3
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Mon Jul 3 09:48:45 2023 +0200

    adapts 'builtin' and 'stubs' packages to latest changes in Viper

commit bb3610b
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Mon Jul 3 09:02:29 2023 +0200

    fixes a typo

commit a18c450
Author: ArquintL <ArquintL@users.noreply.github.com>
Date:   Sat Jul 1 06:00:52 2023 +0000

    Updates submodules

commit 50f379c
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Fri Jun 30 16:47:10 2023 +0200

    fixes unit tests by making type-check caching specific to the config's choice of 32 or 64bit ints

commit 52317a4
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Fri Jun 30 15:48:17 2023 +0200

    fixes compilation errors

commit cda37bc
Merge: 7f32830 4393ad0
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Fri Jun 30 14:50:54 2023 +0200

    Merges branch 'master' into 'pre-parse-unit-tests'

commit 7f32830
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Fri Jun 30 14:43:24 2023 +0200

    cleanup

commit e97cbf5
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Fri Jun 30 11:22:00 2023 +0200

    pre-parses and pre-typeChecks Gobra tests

commit 6f41997
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Fri Jun 30 09:51:57 2023 +0200

    addresses several unit test errors

commit 8d24c01
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Thu Jun 29 17:02:23 2023 +0200

    fixes compilation issue and undos parser caching for unit tests

commit 046fe54
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Thu Jun 29 16:43:04 2023 +0200

    unifies job managers for parsing and type-checking and for the 3 modes

commit 4393ad0
Author: viper-admin <59963956+viper-admin@users.noreply.github.com>
Date:   Wed May 31 20:13:50 2023 +0200

    Updates submodules (viperproject#657)

    Co-authored-by: jcp19 <jcp19@users.noreply.github.com>

commit ed3aaf4
Author: Felix Wolf <60103963+Felalolf@users.noreply.github.com>
Date:   Wed May 31 20:13:16 2023 +0200

    Fix viperproject#655 (viperproject#656)

    * Fix viperproject#655

    * fixed reintroduced bug

commit 5aa73b1
Author: viper-admin <59963956+viper-admin@users.noreply.github.com>
Date:   Fri May 19 15:45:09 2023 +0200

    Updates submodules (viperproject#654)

    Co-authored-by: jcp19 <jcp19@users.noreply.github.com>

commit 5aeb8bf
Author: viper-admin <59963956+viper-admin@users.noreply.github.com>
Date:   Tue May 16 12:02:56 2023 +0200

    Updates submodules (viperproject#653)

    Co-authored-by: jcp19 <jcp19@users.noreply.github.com>

commit 178f985
Author: João Pereira <joaopereira.19@gmail.com>
Date:   Sun May 14 17:35:44 2023 +0200

    Fix issue 651 (viperproject#652)

    * Add bug witness

    * Add fix

    * Reflect that the order of fields matter in the signature of AdtClauseT

    * use more general type

commit 3ce34f3
Author: viper-admin <59963956+viper-admin@users.noreply.github.com>
Date:   Fri May 12 16:59:46 2023 +0200

    Updates submodules (viperproject#650)

    Co-authored-by: jcp19 <jcp19@users.noreply.github.com>

commit c0e1c40
Author: João Pereira <joaopereira.19@gmail.com>
Date:   Thu May 11 19:50:47 2023 +0200

    Update tutorial.md (viperproject#603)

commit f4babde
Author: viper-admin <59963956+viper-admin@users.noreply.github.com>
Date:   Fri May 5 18:38:26 2023 +0200

    Updates submodules (viperproject#648)

    Co-authored-by: jcp19 <jcp19@users.noreply.github.com>

commit 686b53d
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Mar 14 11:23:54 2023 +0100

    Parses all inputs to 'GobraTests' in parallel before actually starting the unit tests

commit c00c636
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Thu Mar 30 14:02:13 2023 +0200

    adds a sequential parser

commit cfed2ce
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Thu Mar 30 09:50:34 2023 +0200

    fixes reporting of errors in imported packages and reports them as part of type-checking

commit 169d091
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Wed Mar 15 19:46:48 2023 +0100

    fixes parser error messages

commit ba5f161
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Mar 14 17:59:26 2023 +0100

    cleans up

commit 3ed1598
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Mar 14 17:36:43 2023 +0100

    fixes unit tests

commit 66f542d
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Mar 14 08:56:09 2023 +0100

    Revert "restricts unit tests to 'regressions/features/header_only'"

    This reverts commit 53453f0.

commit 9edc26e
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Tue Mar 14 08:54:47 2023 +0100

    propagates parsing exceptions, built-in files are always considered even with  enabled

commit 53453f0
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Mon Mar 13 14:21:29 2023 +0100

    restricts unit tests to 'regressions/features/header_only'

commit 04874c9
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Fri Mar 10 16:02:12 2023 +0100

    fixes a unit test

commit a2b9b6c
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Fri Mar 10 15:43:46 2023 +0100

    adds PPackage caching to parser

commit a45f58c
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Thu Mar 9 15:12:10 2023 +0100

    fixes license headers

commit db26519
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Thu Mar 9 15:10:54 2023 +0100

    fixes license headers

commit 5a4f353
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Thu Mar 9 15:07:44 2023 +0100

    fixes unit tests

commit 81ea403
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Thu Mar 9 09:38:03 2023 +0100

    saves ongoing work

commit 8039bcf
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Thu Mar 9 09:32:22 2023 +0100

    updates ANTLR Go lexer and parser

commit 62d6349
Author: Linard Arquint <linard.arquint@inf.ethz.ch>
Date:   Sat Mar 4 20:22:55 2023 +0100

    saves on-going work
  • Loading branch information
@koflin
koflin committed Aug 18, 2023
1 parent 2dd2a9c commit 63b26cf
Show file tree
Hide file tree
Showing 65 changed files with 1,268 additions and 429 deletions.
1 change: 1 addition & 0 deletions build.sbt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ lazy val gobra = (project in file("."))
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.12.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
Expand Down
4 changes: 2 additions & 2 deletions docs/tutorial.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -401,7 +401,7 @@ pure func toSeq(s []int) (res seq[int]) {

Gobra supports many of Go's native types, namely integers (`int`, `int8`, `int16`, `int32`, `int64`, `byte`, `uint8`, `rune`, `uint16`, `uint32`, `uint64`, `uintptr`), strings, structs, pointers, arrays, slices, interfaces, and channels. Note that currently the support for strings and specific types of integers such as `rune` is very limited.

In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`|set1|`).
In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`len(set1)`).


## Interfaces
Expand Down Expand Up @@ -680,4 +680,4 @@ java -Xss128m -jar gobra.jar -i [FILES_TO_VERIFY]
To check the full list of flags available in Gobra, run the command
```bash
java -jar gobra.jar -h
```
```
24 changes: 20 additions & 4 deletions src/main/antlr4/GoLexer.g4
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -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);
Expand All @@ -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]
Expand All @@ -229,6 +240,7 @@ fragment UNICODE_DIGIT
| [\u1810-\u1819]
| [\uFF10-\uFF19]*/
;
fragment UNICODE_LETTER
: [\p{L}]
/* [\u0041-\u005A]
Expand Down Expand Up @@ -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
Expand All @@ -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);
7 changes: 4 additions & 3 deletions src/main/antlr4/GoParser.g4
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ varSpec:

block: L_CURLY statementList? R_CURLY;

statementList: (statement eos)+;
statementList: ((SEMI? | EOS? | {this.closingBracket()}?) statement eos)+;

statement:
declaration
Expand Down Expand Up @@ -193,7 +193,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?;
Expand Down Expand Up @@ -399,4 +399,5 @@ eos:
SEMI
| EOF
| EOS
| {closingBracket()}?;
| {this.closingBracket()}?
;
4 changes: 4 additions & 0 deletions src/main/antlr4/GobraParser.g4
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
7 changes: 7 additions & 0 deletions src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitSourceFile(GobraParser.SourceFileContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
* <p>The default implementation returns the result of calling
* {@link #visitChildren} on {@code ctx}.</p>
*/
@Override public T visitPreamble(GobraParser.PreambleContext ctx) { return visitChildren(ctx); }
/**
* {@inheritDoc}
*
Expand Down
1 change: 1 addition & 0 deletions src/main/resources/stubs/strconv/atoi.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ pure func (e *NumError) Unwrap() error { return e.Err }
ghost
requires exp >= 0
ensures res == (exp == 0 ? 1 : (base * Exp(base, exp - 1)))
decreases exp
pure func Exp(base int, exp int) (res int) {
return exp == 0 ? 1 : (base * Exp(base, exp - 1))
}
Expand Down
1 change: 1 addition & 0 deletions src/main/resources/stubs/strings/strings.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,7 @@ func Map(mapping func(rune) rune, s string) string
// the result of (len(s) * count) overflows.
requires count >= 0
ensures res == (count == 0? "" : s + Repeat(s, count - 1))
decreases count
pure func Repeat(s string, count int) (res string) /*{
if count == 0 {
return ""
Expand Down
119 changes: 71 additions & 48 deletions src/main/scala/viper/gobra/Gobra.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,18 @@
package viper.gobra

import ch.qos.logback.classic.Logger
import scalaz.EitherT

import java.nio.file.Paths
import java.util.concurrent.ExecutionException
import com.typesafe.scalalogging.StrictLogging
import org.slf4j.LoggerFactory
import viper.gobra.ast.frontend.PPackage
import scalaz.Scalaz.futureInstance
import viper.gobra.ast.internal.Program
import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform, OverflowChecksTransform}
import viper.gobra.backend.BackendVerifier
import viper.gobra.frontend.PackageResolver.{AbstractPackage, RegularPackage}
import viper.gobra.frontend.Parser.ParseResult
import viper.gobra.frontend.info.{Info, TypeInfo}
import viper.gobra.frontend.{Config, Desugar, PackageInfo, Parser, ScallopGobraConfig}
import viper.gobra.reporting._
Expand Down Expand Up @@ -140,7 +143,7 @@ trait GoVerifier extends StrictLogging {
if (allErrors.isEmpty) VerifierResult.Success else VerifierResult.Failure(allErrors)
}

protected[this] def verify(pkgInfo: PackageInfo, config: Config)(executor: GobraExecutionContext): Future[VerifierResult]
protected[this] def verify(pkgInfo: PackageInfo, config: Config)(implicit executor: GobraExecutionContext): Future[VerifierResult]
}

trait GoIdeVerifier {
Expand All @@ -149,34 +152,30 @@ trait GoIdeVerifier {

class Gobra extends GoVerifier with GoIdeVerifier {

override def verify(pkgInfo: PackageInfo, config: Config)(executor: GobraExecutionContext): Future[VerifierResult] = {
// directly declaring the parameter implicit somehow does not work as the compiler is unable to spot the inheritance
implicit val _executor: GobraExecutionContext = executor

val task = Future {
for {
finalConfig <- getAndMergeInFileConfig(config, pkgInfo)
_ = setLogLevel(finalConfig)
parsedPackage <- performParsing(pkgInfo, finalConfig)
typeInfo <- performTypeChecking(parsedPackage, finalConfig)
program <- performDesugaring(parsedPackage, typeInfo, finalConfig)
program <- performInternalTransformations(program, finalConfig, pkgInfo)
viperTask <- performViperEncoding(program, finalConfig, pkgInfo)
} yield (viperTask, finalConfig)
}

task.flatMap{
case Left(Vector()) => Future(VerifierResult.Success)
case Left(errors) => Future(VerifierResult.Failure(errors))
case Right((job, finalConfig)) => performVerification(finalConfig, pkgInfo, job.program, job.backtrack)(executor)
}
override def verify(pkgInfo: PackageInfo, config: Config)(implicit executor: GobraExecutionContext): Future[VerifierResult] = {
val task = for {
finalConfig <- EitherT.fromEither(Future.successful(getAndMergeInFileConfig(config, pkgInfo)))
_ = setLogLevel(finalConfig)
parseResults <- performParsing(finalConfig, pkgInfo)
typeInfo <- performTypeChecking(finalConfig, pkgInfo, parseResults)
program <- performDesugaring(finalConfig, typeInfo)
program <- performInternalTransformations(finalConfig, pkgInfo, program)
viperTask <- performViperEncoding(finalConfig, pkgInfo, program)
} yield (viperTask, finalConfig)

task.foldM({
case Vector() => Future(VerifierResult.Success)
case errors => Future(VerifierResult.Failure(errors))
}, {
case (job, finalConfig) => performVerification(finalConfig, pkgInfo, job.program, job.backtrack)
})
}

override def verifyAst(config: Config, pkgInfo: PackageInfo, ast: vpr.Program, backtrack: BackTranslator.BackTrackInfo)(executor: GobraExecutionContext): Future[VerifierResult] = {
// directly declaring the parameter implicit somehow does not work as the compiler is unable to spot the inheritance
implicit val _executor: GobraExecutionContext = executor
val viperTask = BackendVerifier.Task(ast, backtrack)
performVerification(viperTask, config, pkgInfo)
performVerification(config, pkgInfo, viperTask)
.map(BackTranslator.backTranslate(_)(config))
.recoverWith {
case e: ExecutionException if isKnownZ3Bug(e) =>
Expand Down Expand Up @@ -241,65 +240,89 @@ class Gobra extends GoVerifier with GoIdeVerifier {
.setLevel(config.logLevel)
}

private def performParsing(pkgInfo: PackageInfo, config: Config): Either[Vector[VerifierError], PPackage] = {
// returns `Left(...)` if parsing of the package identified by `pkgInfo` failed. Note that `Right(...)` does not imply
// that all imported packages have been parsed successfully (this is only checked during type-checking)
private def performParsing(config: Config, pkgInfo: PackageInfo)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, Map[AbstractPackage, ParseResult]] = {
if (config.shouldParse) {
val sourcesToParse = config.packageInfoInputMap(pkgInfo)
Parser.parse(sourcesToParse, pkgInfo)(config)
val startMs = System.currentTimeMillis()
val res = Parser.parse(config, pkgInfo)
logger.debug {
val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
s"parser phase done, took ${durationS}s"
}
res
} else {
Left(Vector())
EitherT.left(Vector.empty)
}
}

private def performTypeChecking(parsedPackage: PPackage, config: Config): Either[Vector[VerifierError], TypeInfo] = {
private def performTypeChecking(config: Config, pkgInfo: PackageInfo, parseResults: Map[AbstractPackage, ParseResult])(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, TypeInfo] = {
if (config.shouldTypeCheck) {
Info.check(parsedPackage, config.packageInfoInputMap(parsedPackage.info), isMainContext = true)(config)
Info.check(config, RegularPackage(pkgInfo.id), parseResults)
} else {
Left(Vector())
EitherT.left(Vector.empty)
}
}

private def performDesugaring(parsedPackage: PPackage, typeInfo: TypeInfo, config: Config): Either[Vector[VerifierError], Program] = {
private def performDesugaring(config: Config, typeInfo: TypeInfo)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, Program] = {
if (config.shouldDesugar) {
Right(Desugar.desugar(parsedPackage, typeInfo)(config))
} else {
Left(Vector())
}
}

private def performVerification(config: Config, pkgInfo: PackageInfo, ast: vpr.Program, backtrack: BackTranslator.BackTrackInfo)(executor: GobraExecutionContext): Future[VerifierResult] = {
if (config.noVerify) {
Future(VerifierResult.Success)(executor)
val startMs = System.currentTimeMillis()
val res = EitherT.right[Vector[VerifierError], Future, Program](Desugar.desugar(config, typeInfo)(executor))
logger.debug {
val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
s"desugaring done, took ${durationS}s"
}
res
} else {
verifyAst(config, pkgInfo, ast, backtrack)(executor)
EitherT.left(Vector.empty)
}
}

/**
* Applies transformations to programs in the internal language. Currently, only adds overflow checks but it can
* be easily extended to perform more transformations
*/
private def performInternalTransformations(program: Program, config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], Program] = {
private def performInternalTransformations(config: Config, pkgInfo: PackageInfo, program: Program)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, Program] = {
// constant propagation does not cause duplication of verification errors caused
// by overflow checks (if enabled) because all overflows in constant declarations
// can be found by the well-formedness checks.
val startMs = System.currentTimeMillis()
var transformations: Vector[InternalTransform] = Vector(CGEdgesTerminationTransform, ConstantPropagation)
if (config.checkOverflows) {
transformations :+= OverflowChecksTransform
}
val result = transformations.foldLeft(program)((prog, transf) => transf.transform(prog))
logger.debug {
val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
s"internal transformations done, took ${durationS}s"
}
config.reporter.report(AppliedInternalTransformsMessage(config.packageInfoInputMap(pkgInfo).map(_.name), () => result))
Right(result)
EitherT.right(result)
}

private def performViperEncoding(program: Program, config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], BackendVerifier.Task] = {
private def performViperEncoding(config: Config, pkgInfo: PackageInfo, program: Program)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, BackendVerifier.Task] = {
if (config.shouldViperEncode) {
Right(Translator.translate(program, pkgInfo)(config))
val startMs = System.currentTimeMillis()
val res = EitherT.fromEither[Future, Vector[VerifierError], BackendVerifier.Task](Future.successful(Translator.translate(program, pkgInfo)(config)))
logger.debug {
val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
s"Viper encoding done, took ${durationS}s"
}
res
} else {
EitherT.left(Vector.empty)
}
}

private def performVerification(config: Config, pkgInfo: PackageInfo, ast: vpr.Program, backtrack: BackTranslator.BackTrackInfo)(implicit executor: GobraExecutionContext): Future[VerifierResult] = {
if (config.noVerify) {
Future(VerifierResult.Success)(executor)
} else {
Left(Vector())
verifyAst(config, pkgInfo, ast, backtrack)(executor)
}
}

private def performVerification(viperTask: BackendVerifier.Task, config: Config, pkgInfo: PackageInfo)(implicit executor: GobraExecutionContext): Future[BackendVerifier.Result] = {
private def performVerification(config: Config, pkgInfo: PackageInfo, viperTask: BackendVerifier.Task)(implicit executor: GobraExecutionContext): Future[BackendVerifier.Result] = {
if (config.shouldVerify) {
BackendVerifier.verify(viperTask, pkgInfo)(config)
} else {
Expand Down
Loading

0 comments on commit 63b26cf

Please sign in to comment.