viperproject / viperserver Goto Github PK

Progress in ViperServer is measured by #verifiedMember/#totalMembers. The total number of members is taken from the parsed AST before the termination plugin does its transformations.

These transformations create additional methods that prove the termination. These additional methods return verification results, which then increment the number of verified members, possibly above the total number in the original program.

Pull request 🔀 created by bitbucket user rukaelin on 2017-05-09 14:30
Last updated on 2017-05-11 16:13
Original Bitbucket pull request id: 3

Participants:

• @aterga (reviewer)

Source: 1b1d187 on branch rukaelin/viperserver_for_ide/default
Destination: 9acb8d1 on branch master
Marge commit: 1b1d187

State: MERGED

• added flushCache functionality, fixed timeout problems

• implemented backend specific cache

• fixed error location updating, implemented backendSpecific cache, implemented cacheFlushing, removed entityHash from Info, added timestamp and backendName to CacheEntry

• fix for problem with Quantifiers

• fix for update error location

• fix for update error location

• fix for autotriggers and other improvements

• deal with the missing copy method of the DomainFuncApp case class

• (easterEgg commit) implemented goto Definition

• ViperCache.scala edited online with Bitbucket

After upgrading many different dependencies in Viper, including ScalaTest, a few regression tests in ViperServer are halting in busy waiting state. They were temporarily commented out in file: src/test/scala/CoreServerTests.scala.

This issue is to address what's going on in such tests and to uncomment those tests.

Using the following JDK in a GitHub action results in non-deterministic failures of AsyncCoreServerSpec test cases. They seem to be caused by Silicon being interrupted and cannot be reproduced locally.

The following step is used to install the mentioned JDK version:

- name: Set up JDK 15
  uses: actions/setup-java@v1
  with:
    java-version: '15.0.1'
    architecture: x64

Gobra Server has emitted the following error during CI on a Windows machine:

[scallop] Error: Validation failure for 'port' option parameters: 

Gobra Server was configured to use port 50009 but this port configuration is handled by Gobra Server and is not forwarded to ViperCoreServer (we pass an empty array of args to ViperCoreServer).
However, I couldn't find any other component that could cause the above error and I suspect ViperConfig somehow being unable to find a free port (which is the default behavior).
As ViperCoreServer does not seem to use any port (which is also not a task for ViperCoreServer), I request to remove this config option from ViperConfig and maybe move it to a separate config (e.g. ViperHttpConfig).
As part of this change, one could strip ViperConfig down to the minimum set of options that ViperCoreServer needs (and therefore call it ViperCoreServerConfig).

Pull request 🔀 created by @fabiopakk on 2018-10-31 15:45
Last updated on 2019-01-29 14:47
Original Bitbucket pull request id: 8

Participants:

• @alexanderjsummers (reviewer)
• @aterga (reviewer)
• @mschwerhoff (reviewer) ✔️
• @fabiopakk

Source: 5beaf1a on branch fabiopakk_dependencies_update
Destination: 9d5937d on branch master
Marge commit: 9145a09

State: MERGED

• Upgraded SBT to 1.2.1, Scala to 2.12 and all libraries to latest version to this date. Build.sbt entirely rewritten with new configuration syntax.
• Warnings cleanup.
• Upgraded SBT, sbt-assembly versions and cleanup build configuration files.

As a result of a recent student project, we have a new (prototype) frontend to ViperServer, based on LSP, that complements the existing Http frontend. Using this frontend in the production version of Viper IDE would allow simplifying and improve the infrastructure since we wouldn't need a custom Http client implemented in Typescript on the VS Code side.

To make this happen, there are the following steps:

1. Review and merge the PR for Viper IDE (viperproject/viper-ide#113)
2. Learn how to efficiently debug the LSP frontend. Currently one needs to assemble a fat JAR and run the VS Code extension in order to start up the LSP server. There must be a way to attach to a version of the LSP server that was started by e.g. SBT; that would simplify the development cycle.
3. Test and debug thorougly, to make sure that the new solution is production-ready.

Pull request 🔀 created by bitbucket user rukaelin on 2017-05-04 07:15
Last updated on 2017-05-04 07:20
Original Bitbucket pull request id: 2

Participants:

• @aterga (reviewer)

Source: 9acb8d1 on branch rukaelin/viperserver_for_ide/default
Destination: f1daddd on branch master
Marge commit: 9acb8d1

State: MERGED

improved the stability of the ViperServer
improved the shutdown behaviour.
added support for sbt stage

When the backend crashes unexpectedly, the output from Viper Server includes messages such as:

The command carbon --z3Exe c:\Users\Alex Summers\AppData\Roaming\Code\User\globalStorage\viper-admin.viper\Nightly\ViperTools\z3\bin\z3.exe --boogieExe c:\Users\Alex Summers\AppData\Roaming\Code\User\globalStorage\viper-admin.viper\Nightly\ViperTools\boogie\Binaries\Boogie.exe resulted in an exception.

It would be great if this could be improved by (a) including quotes etc. around paths (as they are presumably written in the underlying command) and (b) including the (properly quoted) path to the file being verified. This way, the output could be taken and rerun locally when debugging (and potential confusion with the paths looking broken could be avoided, of course!).

Pull request 🔀 created by @aterga on 2018-03-31 13:49
Last updated on 2018-05-10 21:09
Original Bitbucket pull request id: 5

Participants:

• @aterga
• @vakaras (reviewer)

Source: 6dde360 on branch arshavir/viperserver-dynamic-backends/default
Destination: f2979f6 on branch master
Marge commit: 6dde360

State: MERGED

• Increased the maximum number of messages in the reporter's message buffer (from 100 to 1000).

• Added support for dynamically loading verification beckends (SilFrontend implementations).

• Update the logger dependencies (entirely switch to pure logback since customization beyond scala-logging is needed anyway).

• Implemented JSON marshaller for reporter.ExceptionReport

• Impelmented proper logging; exceptions in verification backends are sent to the IDE via reporter.ExceptionReport.

• Support SilFrontend implementations with the second constructor argument (i.e., reporter) in dynamic verification backend support.

• Implement getLogFileWithGuarantee(): log file will be created in case a writable directory is passed via --logFile.

• Changed the order of prints in ViperServerRunner.main (for IDE compatibility).

When ViperServer retrieves and reports cached verification failures, it should also report the counterexamples that were produced for the cached verification attempts. Currently, this is not the case.

To reproduce, start ViperServer as usual, copy the port number, and send the following verification requests using viper_client — twice:

./client.py -p 54292 -f /Users/wi/viper/viper_client/models/test.vpr -x "--counterexample native"

After the first run, you'll see a response that starts like this:

{
  "msg_body": {
    "details": {
      "result": {
        "errors": [
          {
            "cached": false,
            "counterexample": {
              "model": {
                "$FVF.loc_FIELD_VAL": {
                  "cases": [],
                  "default": {
                    "type": "constant_entry",
                    "value": "true"
                  },
                  "type": "map_entry"
                },
         ...

After the second run, the entire verification result will be just this:

{
  "msg_body": {
    "details": {
      "cached": true,
      "entity": {
        "name": "test",
        "position": {
          "end": "13:1",
          "file": "/Users/wi/viper/viper_client/models/test.vpr",
          "start": "3:12"
        },
        "type": "method"
      },
      "result": {
        "errors": [
          {
            "cached": false,
            "position": {
              "end": "10:9",
              "file": "/Users/wi/viper/viper_client/models/test.vpr",
              "start": "10:8"
            },
            "tag": "assert.failed:assertion.false",
            "text": "Assert might fail. Assertion (NODE_X.FIELD_VAL in FOOTPRINT) might not hold. ([email protected])"
          }
        ],
        "type": "error"
      },
      "time": 0
    },
    "kind": "for_entity",
    "status": "failure",
    "verifier": "silicon"
  },
  "msg_type": "verification_result"
}

In Prusti we use the Viper JARs provided by the ViperServer artifact. Recently, we started getting the following message on stdout:

SLF4J: Class path contains multiple SLF4J bindings.
SLF4J: Found binding in [jar:file:/home/runner/work/prusti-dev/prusti-dev/viper_tools/backends/silicon.jar!/org/slf4j/impl/StaticLoggerBinder.class]
SLF4J: Found binding in [jar:file:/home/runner/work/prusti-dev/prusti-dev/viper_tools/backends/ch.qos.logback.logback-classic-1.2.3.jar!/org/slf4j/impl/StaticLoggerBinder.class]
SLF4J: See http://www.slf4j.org/codes.html#multiple_bindings for an explanation.
SLF4J: Actual binding is of type [ch.qos.logback.classic.util.ContextSelectorStaticBinder]

Apparently, the same class is in multiple JARs. I suspect that this is caused by the recent changes to Viper's build system.

The current version of Github CI for ViperServer is prototypical. This issue can serve as an umbrella for collecting to-dos in the context of CI.

In particular, we determine a reasonable policy for producing and storing nightly and stable releases. Link to the discussion.

The current implementation uses busy waiting that should be eliminated in favor of future handlers, etc.

I want to understand if the current implementation of streamMessages actually streams messages as soon as they are available in the source queue, or is it the case that the streaming starts only when the future returned by lookupJob is complete.

Concretely, here is the code snippet:

    lookupJob(jid) match {
      case Some(handle_future) =>
        handle_future.onComplete({
          case Success(handle) =>
            Source.fromPublisher(handle.publisher).runWith(Sink.actorRef(clientActor, Success))
            _termActor ! Terminator.WatchJobQueue(jid, handle)
          case Failure(e) => clientActor ! e
        })

It seems that the materialization (i.e. the call to runWith) only happens after the future is completed. Shouldn't we first start the stream, then finalize it once the job is completed?

See full code here:

Pull request 🔀 created by @aterga on 2017-10-15 20:53
Last updated on 2017-10-15 20:54
Original Bitbucket pull request id: 4

Source: f92ba13 on branch http-server
Destination: 51c8f9c on branch master
Marge commit: 48e1528

State: MERGED

• Save progress: multi-job infrastructure sketched, but buggy (runtime exceptions in Future[SourceQueue], etc).

• Figured out and fixed the problem with Future[SourceQueueWithComplete].

• Add ViperIDEProtocol.scala; implement common json formatters.

• Fix caching (bug caused by making the AST immutable). Changed Json streaming style.

• Fixed MergeStrategy for fat jar assembly.

• Adapt ViperServer for the new Reporter. Fix some minor bugs.

• Fixed the json writers.

• Fixes and improvements in ViperIDEProtocol.

• [Minor] edit exeption message.

• Implement dynamic message queue for concurrent JSON streaming in Viper Server.

• Supported file paths with whitespaces. Renamed '_main_actor' as '_job_handles'.

• Add interruption handling for verification jobs.

• Reporting AST statistics and program outline.

• Added src/main/resources/application.conf

The following program verifies with standard Silicon and Carbon, but does not verify in VSCode (with an up to date version of Viper):

adt List[T] {
    Nil()
    Cons(elem: T, next: List[T])
}

adt Pair[S,T] {
    MkPair(fst: S, snd: T)
}

domain ListDomain[T] {
    function length(List[T]): Int

    axiom {
        length((Nil(): List[T])) == 0
    }

    axiom {
        forall l: List[T], e: T :: length(Cons(e, l)) == 1 + length(l)
    }
}

method zip(l1: List[Int], l2: List[Int]) returns (res: List[Pair[Int, Int]])
    decreases l1
    ensures length(l1) == length(l2) ==> length(res) == length(l1)
{

    if(l1 == Nil() || l2 == Nil()) {
        res := Nil()
    } else {
        var rest: List[Pair[Int, Int]] := zip(l1.next, l2.next)
        res := Cons(MkPair(l1.elem, l2.elem), rest)
    }
}

I'm reasonably sure that the problem is that the ADT plugin does not generate the well-foundedness axioms for the List type, and that may be because it does not get a config object that says that the termination plugin is active. So this seems potentially related to #165.

When using the VSCode extension for Viper, I first get an error at the last line of this method, which is the expected behavior. However, when I verify the file a second time, I get a spurious error reported: The first assert x == 5, which should hold. I think this is due to how the server caches errors.

method wrong_assertion_false_when_cached() {
    var x: Int := 5
    assert x == 5 // Wrong cached error reported here
    x := 3
    assert x == 5 // Error here
}

Using either Stable or Nightly from the VSCode extension I can't run carbon on a new Windows machine. The ViperServer output includes:

2:14:52.876 The command `carbon --z3Exe c:\Users\Alex Summers\AppData\Roaming\Code\User\globalStorage\viper-admin.viper\Nightly\ViperTools\z3\bin\z3.exe --boogieExe c:\Users\Alex Summers\AppData\Roaming\Code\User\globalStorage\viper-admin.viper\Nightly\ViperTools\boogie\Binaries\Boogie.exe` resulted in an exception.

I can't see the exception, but it looks to me as though the space in "Alex Summers" (which is unfortunate as a user name) might be tripping this up; at least if the printed command is accurate this seems unlikely to work as is.

The following code computes program statistics for a Viper AST.

It should therefore be moved to the Silver repository.

The order of domain functions and domain axioms in a domain should not influence the cacheing behavior in particular because axioms are treated as a global dependency. The current sorting of dependency hashes does not address this problem because domain functions and domain axioms must be sorted before calculating the domain's hash

Currently, the trailing option in the list of arguments must be an existing Viper file; otherwise, SilFrontend will complain while checking the command-line options. However, SilFrontend should not care about the existence of a file in the scenario of ViperServer as we already read the file, parsed it, and constructed a Viper AST based on it. Hence, we should tell it to ignore the checks that it normally performs over files. Fortunately, there's already an option for that, called --ignoreFile.

We should add this option in the execute method of ViperBackend. It should be the second-last element in the list, where the last element is programID. This can be done using pattern matching over the structure of the list.

See https://github.com/viperproject/silver/blob/47ede88df9fb7f25092c8a7064b19468bf78b8bb/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala for more details.

Pull request 🔀 created by bitbucket user aurecchia on 2018-05-24 12:19
Last updated on 2018-07-09 12:42
Original Bitbucket pull request id: 6

Participants:

• @aterga (reviewer)
• bitbucket user aurecchia

Source: cca2a72 on branch aurecchia/viperserver/default
Destination: 85d5914 on branch master

State: DECLINED

Pull request 🔀 created by bitbucket user rukaelin on 2017-04-28 09:37
Last updated on 2017-05-02 10:57
Original Bitbucket pull request id: 1

Participants:

• @aterga (reviewer)

Source: f1daddd on branch rukaelin/viperserver_for_ide/default
Destination: b9c1595 on branch master
Marge commit: f1daddd

State: MERGED

The Viper Server runs as a server and is able to run verifications using either silicon or carbon. Parallel verifications are not supported.
The Viper Server provides a cache to store the verification results of methods. When there are no changes in the AST, the verification is skipped, the cached errors are updated based on the new AST and reported.

Caching can be disabled using the --disableCaching flag

When using the HTTP server I get java.lang.NullPointerException: Cannot invoke "scala.Option.foreach(scala.Function1)" because the return value of "viper.server.core.ViperCache$._cacheFile()" is null as the last event after calling /verify/0 using the Silicon backend.

I tried to look into it and the ViperCache.initialize does not seem to be called at any point in the execution. It seems this should have been called by ViperCoreServer.start which maybe should have been called by ViperHttpServer.start. I've verified that ViperHttpServer.start is called, and it calls super.start so I would have thought that this called ViperCoreServer.start since it extends from it? I don't know Scala so this might all be incorrect :)

Minimal reproduction

The following bash script triggers the issue. It assumes z3 is in the PATH and VIPERSERVER should probably be changed to point to the correct JAR.

#!/bin/bash

set -xe

trap 'kill $(jobs -p)' EXIT

VIPERSERVER=target/scala-*/viperserver.jar
export Z3_EXE=$(which z3)

echo "method a() ensures true {}" > tiny.vpr
TINY_FILE=$(realpath tiny.vpr)

java -jar $VIPERSERVER --port 56644 &

sleep 2

curl --location --request POST "http://localhost:56644/verify" \
    --header 'Content-Type: application/json' \
    --data-raw "{\"arg\": \"silicon $TINY_FILE\"}"

sleep 2

curl --location --request GET 'http://localhost:56644/verify/0'

The verification succeeds as expected:

{
  "msg_body": {
    "details": {
      "cached": false,
      "entity": {
        "name": "a",
        "position": {
          "end": "1:27",
          "file": "tiny.vpr",
          "start": "1:1"
        },
        "type": "method"
      },
      "time": 29
    },
    "kind": "for_entity",
    "status": "success",
    "verifier": "silicon"
  },
  "msg_type": "verification_result"
}

But the final message returned is the NullPointerException:

{
  "msg_body": {
    "message": "java.lang.NullPointerException: Cannot invoke \"scala.Option.foreach(scala.Function1)\" because the return value of \"viper.server.core.ViperCache$._cacheFile()\" is null",
    "stacktrace": [
      "viper.server.core.ViperCache$.writeToFile(ViperCache.scala:282)",
      "viper.server.core.ViperBackend.postCaching(VerificationWorker.scala:301)",
      "viper.server.core.ViperBackend.$anonfun$execute$4(VerificationWorker.scala:154)",
      "scala.util.Either.map(Either.scala:382)",
      "viper.server.core.ViperBackend.$anonfun$execute$3(VerificationWorker.scala:153)",
      "scala.util.Either.flatMap(Either.scala:352)",
      "viper.server.core.ViperBackend.$anonfun$execute$1(VerificationWorker.scala:151)",
      "scala.util.Either.flatMap(Either.scala:352)",
      "viper.server.core.ViperBackend.execute(VerificationWorker.scala:150)",
      "viper.server.core.VerificationWorker.run(VerificationWorker.scala:65)",
      "viper.server.core.VerificationWorker.call(VerificationWorker.scala:106)",
      "viper.server.core.VerificationWorker.call(VerificationWorker.scala:30)",
      "java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)",
      "java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)",
      "java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)",
      "java.base/java.lang.Thread.run(Thread.java:1589)"
    ]
  },
  "msg_type": "exception_report"
}

The issue is still there with --cacheFile set on the call to viperserver.jar.

Using the --plugin option in verificationBackends customArguments does not load the plugin. I looked into the code and there seems to be a ASTGenerator class that loads all the plugins prior to any verifier. However, this means the verifier args like --plugin are not considered, and only the default plugins in Silver are loaded.

For example:

"viperSettings.verificationBackends": [
        {
            "v": "674a514867b1",
            "name": "silicon",
            "type": "silicon",
            "paths": [],
            "engine": "ViperServer",
            "timeout": 100000,
            "stages": [
                {
                    "name": "verify",
                    "isVerification": true,
                    "mainMethod": "viper.silicon.SiliconRunner",
                    "customArguments": "--plugin someRandomPluginClass --z3Exe $z3Exe$ $disableCaching$ $fileToVerify$"
                }
            ],
            "stoppingTimeout": 5000
        }]

The argument provided to --plugin is ignored entirely. Even providing a non-existent class does not have an effect, and there are no error messages.

Pull request 🔀 created by bitbucket user aurecchia on 2018-09-09 18:26
Last updated on 2019-04-23 16:42
Original Bitbucket pull request id: 7

Participants:

• @aterga (reviewer)
• bitbucket user aurecchia

Source: fb6266b on branch aurecchia/viperserver/debugger-support
Destination: fdad473 on branch master
Marge commit: 636c96f

State: MERGED

• Rewrite JSON generation for SymbExLogReport using spray-json.
• Remove non-needed (and wrong) import.
• Fix typo.
• Implement term writer for path condtitions in SymbExLog report.
• Make trace report more generic.
• Check the actual config before writing the trace report.
• Minor tweaks.
• Add structured translation to JSON for heaps.
• Add return sort to applicables in SymbExLogReport.
• Add structured translation to JSON for store.
• Translate the last SMT query to JSON as a proper term.
• Translate sorts to structured JSON objects in SymbExLogReport.
• Change "distinct" contents to symbols as they are not terms.
• Translate sorts to structured objects in the store as well.
• Experimental model generation via Alloy.
• Send back Alloy instance in JSON format.
• Report empty collections in Alloy instance.
• Do not transform Combines with unit.
• Add position to method calls in SymbExLog.
• Remove unused SymbExLog records.
• Add axioms to Symbolic Execution Trace report.
• Report inverse functions for quantified chunks.
• Allow passing the solver backend in Alloy request.
• Report recorded macros in the SymbExLog
• Cleanup state translation in SymbExLog.
• Also report atoms inside each Alloy signature.
• Return functions postconditions in execution trace report.
• Make sure the Alloy configuration corresponds to that of the GUI.
• Align with default options in the GUI.

Verification using Viperserver together with Silicon fails with the following error (unless --ignoreFile is provided):

msg=invalid_args_report(tool_signature=Silicon 1.1-SNAPSHOT (0964fff4+), errors=[Command-line interface: Cannot find file '_programID_failing_post.gobra' from 'file' argument. (<no position>)])

Quick fix: I add the --ignoreFile option to all my verification jobs. However, I think this option should automatically be set when verifying an AST instead of a Viper file