diff --git a/.gitignore b/.gitignore index 847153d70..ba1a7bfff 100644 --- a/.gitignore +++ b/.gitignore @@ -10,6 +10,29 @@ silver silicon viperserver logger.log - +*.log *.go.* -*.gobra.* \ No newline at end of file +*.gobra.* + +playground +.metals +.vscode +.vscode/launch.json +.metals/metals.lock.db +.metals/readonly/scala/package.scala +.metals/metals.h2.db +.metals/metals.log +.vscode/settings.json +project/.bloop +project/.bloop/* +fvf_finder.sh +.gitignore +csv +warmup +congregated_date.ods +.~lock.congregated_date.ods# +asserionerrors +eval_nErrors +n_Errors_2 +replicateFile.sh +numars diff --git a/README.md b/README.md index c25dd83e3..78f22ea0d 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,3 @@ - - [![Test Status](https://github.com/viperproject/gobra/workflows/test/badge.svg?branch=master)](https://github.com/viperproject/gobra/actions?query=workflow%3Atest+branch%3Amaster) [![License: MPL 2.0](https://img.shields.io/badge/License-MPL%202.0-brightgreen.svg)](./LICENSE) diff --git a/project/.bloop/bloop.settings.json b/project/.bloop/bloop.settings.json new file mode 100644 index 000000000..be87d6fe3 --- /dev/null +++ b/project/.bloop/bloop.settings.json @@ -0,0 +1,18 @@ +{ + "semanticDBVersion": "4.4.13", + "supportedScalaVersions": [ + "2.13.5", + "2.12.13", + "2.12.12", + "2.12.11", + "2.12.10", + "2.13.3", + "2.13.4", + "2.11.12", + "2.12.8", + "2.12.9", + "2.13.0", + "2.13.1", + "2.13.2" + ] +} \ No newline at end of file diff --git a/project/.bloop/gobra-build.json b/project/.bloop/gobra-build.json new file mode 100644 index 000000000..00f9c6d2d --- /dev/null +++ b/project/.bloop/gobra-build.json @@ -0,0 +1,2147 @@ +{ + "version": "1.4.0", + "project": { + "name": "gobra-build", + "directory": "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project", + "workspaceDir": "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project", + "sources": [ + "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/src/main/scala", + "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/src/main/scala-2.12", + "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/src/main/scala-2", + "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/src/main/java", + "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/src/main/scala-sbt-1.0", + "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/target/scala-2.12/sbt-1.0/src_managed/main" + ], + "dependencies": [ + + ], + "classpath": [ + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/sbt/1.4.4/sbt-1.4.4.jar", + "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-library.jar", + "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.eed3si9n/sbt-assembly/scala_2.12/sbt_1.0/0.14.8/jars/sbt-assembly.jar", + "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.typesafe.sbt/sbt-native-packager/scala_2.12/sbt_1.0/1.3.12/jars/sbt-native-packager.jar", + "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.eed3si9n/sbt-buildinfo/scala_2.12/sbt_1.0/0.9.0/jars/sbt-buildinfo.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/main_2.12/1.4.4/main_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/io_2.12/1.4.0/io_2.12-1.4.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scalactic/scalactic_2.12/3.0.1/scalactic_2.12-3.0.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/pantsbuild/jarjar/1.6.6/jarjar-1.6.6.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/commons/commons-compress/1.14/commons-compress-1.14.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/ant/ant/1.10.1/ant-1.10.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/spotify/docker-client/8.9.0/docker-client-8.9.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/modules/scala-parser-combinators_2.12/1.1.2/scala-parser-combinators_2.12-1.1.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/modules/scala-xml_2.12/1.3.0/scala-xml_2.12-1.3.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/logic_2.12/1.4.4/logic_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/actions_2.12/1.4.4/actions_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/main-settings_2.12/1.4.4/main-settings_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/run_2.12/1.4.4/run_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/command_2.12/1.4.4/command_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/collections_2.12/1.4.4/collections_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/scripted-plugin_2.12/1.4.4/scripted-plugin_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-lm-integration_2.12/1.4.4/zinc-lm-integration_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-logging_2.12/1.4.4/util-logging_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/launcher-interface/1.1.5/launcher-interface-1.1.5.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/ben-manes/caffeine/caffeine/2.8.5/caffeine-2.8.5.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/io/get-coursier/lm-coursier-shaded_2.12/2.0.3/lm-coursier-shaded_2.12-2.0.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/logging/log4j/log4j-api/2.11.2/log4j-api-2.11.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/logging/log4j/log4j-core/2.11.2/log4j-core-2.11.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/logging/log4j/log4j-slf4j-impl/2.11.2/log4j-slf4j-impl-2.11.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/librarymanagement-core_2.12/1.4.1/librarymanagement-core_2.12-1.4.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/librarymanagement-ivy_2.12/1.4.1/librarymanagement-ivy_2.12-1.4.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/compiler-interface/1.4.3/compiler-interface-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-compile_2.12/1.4.3/zinc-compile_2.12-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/swoval/file-tree-views/2.1.4/file-tree-views-2.1.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/net/java/dev/jna/jna/5.5.0/jna-5.5.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/net/java/dev/jna/jna-platform/5.5.0/jna-platform-5.5.0.jar", + "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-reflect.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm/6.2/asm-6.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm-commons/6.2/asm-commons-6.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/maven/maven-plugin-api/3.3.9/maven-plugin-api-3.3.9.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/ant/ant-launcher/1.10.1/ant-launcher-1.10.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/slf4j/slf4j-api/1.7.26/slf4j-api-1.7.26.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/google/guava/guava/20.0/guava-20.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/jaxrs/jackson-jaxrs-json-provider/2.8.8/jackson-jaxrs-json-provider-2.8.8.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/datatype/jackson-datatype-guava/2.8.8/jackson-datatype-guava-2.8.8.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-databind/2.8.8/jackson-databind-2.8.8.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/core/jersey-client/2.22.2/jersey-client-2.22.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/connectors/jersey-apache-connector/2.22.2/jersey-apache-connector-2.22.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/media/jersey-media-json-jackson/2.22.2/jersey-media-json-jackson-2.22.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/commons-io/commons-io/2.5/commons-io-2.5.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/httpcomponents/httpclient/4.5/httpclient-4.5.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/httpcomponents/httpcore/4.4.5/httpcore-4.4.5.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-unixsocket/0.8/jnr-unixsocket-0.8.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/commons-lang/commons-lang/2.6/commons-lang-2.6.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/bouncycastle/bcpkix-jdk15on/1.52/bcpkix-jdk15on-1.52.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/ch/qos/logback/logback-classic/1.2.1/logback-classic-1.2.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-relation_2.12/1.4.4/util-relation_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/completion_2.12/1.4.4/completion_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/task-system_2.12/1.4.4/task-system_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/tasks_2.12/1.4.4/tasks_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/testing_2.12/1.4.4/testing_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-tracking_2.12/1.4.4/util-tracking_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/sjson-new-scalajson_2.12/0.9.1/sjson-new-scalajson_2.12-0.9.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/jline3/jline-terminal/3.16.0-sbt-211a082ed6326908dc84ca017ce4430728f18a8a/jline-terminal-3.16.0-sbt-211a082ed6326908dc84ca017ce4430728f18a8a.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-classpath_2.12/1.4.3/zinc-classpath_2.12-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-apiinfo_2.12/1.4.3/zinc-apiinfo_2.12-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc_2.12/1.4.3/zinc_2.12-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/core-macros_2.12/1.4.4/core-macros_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-cache_2.12/1.4.4/util-cache_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-control_2.12/1.4.4/util-control_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/protocol_2.12/1.4.4/protocol_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/sjson-new-core_2.12/0.9.1/sjson-new-core_2.12-0.9.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/template-resolver/0.1/template-resolver-0.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-position_2.12/1.4.4/util-position_2.12-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-compile-core_2.12/1.4.3/zinc-compile-core_2.12-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-interface/1.4.4/util-interface-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/jline/jline/2.14.7-sbt-5e51b9d4f9631ebfa29753ce4accc57808e7fd6b/jline-2.14.7-sbt-5e51b9d4f9631ebfa29753ce4accc57808e7fd6b.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-terminal-jna/3.16.0/jline-terminal-jna-3.16.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-terminal-jansi/3.16.0/jline-terminal-jansi-3.16.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/lmax/disruptor/3.4.2/disruptor-3.4.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/checkerframework/checker-qual/3.4.1/checker-qual-3.4.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/google/errorprone/error_prone_annotations/2.4.0/error_prone_annotations-2.4.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/modules/scala-collection-compat_2.12/2.2.0/scala-collection-compat_2.12-2.2.0.jar", + "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-compiler.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/jcraft/jsch/0.1.54/jsch-0.1.54.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/gigahorse-okhttp_2.12/0.5.0/gigahorse-okhttp_2.12-0.5.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/squareup/okhttp3/okhttp-urlconnection/3.7.0/okhttp-urlconnection-3.7.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/ivy/ivy/2.3.0-sbt-fbc4f586aeeb1591710b14eb4f41b94880dcd745/ivy-2.3.0-sbt-fbc4f586aeeb1591710b14eb4f41b94880dcd745.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm-tree/6.2/asm-tree-6.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm-analysis/6.2/asm-analysis-6.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/maven/maven-model/3.3.9/maven-model-3.3.9.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/maven/maven-artifact/3.3.9/maven-artifact-3.3.9.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/eclipse/sisu/org.eclipse.sisu.plexus/0.3.2/org.eclipse.sisu.plexus-0.3.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/jaxrs/jackson-jaxrs-base/2.8.8/jackson-jaxrs-base-2.8.8.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-core/2.8.8/jackson-core-2.8.8.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/module/jackson-module-jaxb-annotations/2.8.8/jackson-module-jaxb-annotations-2.8.8.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-annotations/2.8.0/jackson-annotations-2.8.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/ws/rs/javax.ws.rs-api/2.0.1/javax.ws.rs-api-2.0.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/core/jersey-common/2.22.2/jersey-common-2.22.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/hk2-api/2.4.0-b34/hk2-api-2.4.0-b34.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/external/javax.inject/2.4.0-b34/javax.inject-2.4.0-b34.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/hk2-locator/2.4.0-b34/hk2-locator-2.4.0-b34.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/ext/jersey-entity-filtering/2.22.2/jersey-entity-filtering-2.22.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/commons-logging/commons-logging/1.2/commons-logging-1.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/commons-codec/commons-codec/1.9/commons-codec-1.9.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-ffi/2.0.3/jnr-ffi-2.0.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-constants/0.8.7/jnr-constants-0.8.7.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-enxio/0.9/jnr-enxio-0.9.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-posix/3.0.12/jnr-posix-3.0.12.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/bouncycastle/bcprov-jdk15on/1.52/bcprov-jdk15on-1.52.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/ch/qos/logback/logback-core/1.2.1/logback-core-1.2.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-reader/3.16.0/jline-reader-3.16.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-builtins/3.16.0/jline-builtins-3.16.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/test-agent/1.4.4/test-agent-1.4.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/test-interface/1.0/test-interface-1.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/shaded-jawn-parser_2.12/0.9.1/shaded-jawn-parser_2.12-0.9.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/shaded-scalajson_2.12/1.0.0-M4/shaded-scalajson_2.12-1.0.0-M4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/compiler-bridge_2.12/1.4.3/compiler-bridge_2.12-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-classfile_2.12/1.4.3/zinc-classfile_2.12-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-core_2.12/1.4.3/zinc-core_2.12-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-persist_2.12/1.4.3/zinc-persist_2.12-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/sjson-new-murmurhash_2.12/0.9.1/sjson-new-murmurhash_2.12-0.9.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/ipcsocket/ipcsocket/1.1.0/ipcsocket-1.1.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/net/openhft/zero-allocation-hashing/0.10.1/zero-allocation-hashing-0.10.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/fusesource/jansi/jansi/1.18/jansi-1.18.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-terminal/3.16.0/jline-terminal-3.16.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/gigahorse-core_2.12/0.5.0/gigahorse-core_2.12-0.5.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/squareup/okhttp3/okhttp/3.14.2/okhttp-3.14.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/codehaus/plexus/plexus-utils/3.0.22/plexus-utils-3.0.22.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/commons/commons-lang3/3.4/commons-lang3-3.4.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/enterprise/cdi-api/1.0/cdi-api-1.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/eclipse/sisu/org.eclipse.sisu.inject/0.3.2/org.eclipse.sisu.inject-0.3.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/codehaus/plexus/plexus-component-annotations/1.5.5/plexus-component-annotations-1.5.5.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/codehaus/plexus/plexus-classworlds/2.5.2/plexus-classworlds-2.5.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/annotation/javax.annotation-api/1.2/javax.annotation-api-1.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/bundles/repackaged/jersey-guava/2.22.2/jersey-guava-2.22.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/osgi-resource-locator/1.0.1/osgi-resource-locator-1.0.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/hk2-utils/2.4.0-b34/hk2-utils-2.4.0-b34.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/external/aopalliance-repackaged/2.4.0-b34/aopalliance-repackaged-2.4.0-b34.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/javassist/javassist/3.18.1-GA/javassist-3.18.1-GA.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jffi/1.2.9/jffi-1.2.9.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jffi/1.2.9/jffi-1.2.9-native.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm-util/5.0.3/asm-util-5.0.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-x86asm/1.0.2/jnr-x86asm-1.0.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-style/3.16.0/jline-style-3.16.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-persist-core-assembly/1.4.3/zinc-persist-core-assembly-1.4.3.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/sbinary_2.12/0.5.1/sbinary_2.12-0.5.1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/typesafe/ssl-config-core_2.12/0.4.0/ssl-config-core_2.12-0.4.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/reactivestreams/reactive-streams/1.0.2/reactive-streams-1.0.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/squareup/okio/okio/1.17.2/okio-1.17.2.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/annotation/jsr250-api/1.0/jsr250-api-1.0.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/inject/javax.inject/1/javax.inject-1.jar", + "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/typesafe/config/1.3.3/config-1.3.3.jar" + ], + "out": "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/.bloop/gobra-build", + "classesDir": "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/.bloop/gobra-build/scala-2.12/sbt-1.0/classes", + "resources": [ + "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/src/main/resources", + "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/target/scala-2.12/sbt-1.0/resource_managed/main" + ], + "scala": { + "organization": "org.scala-lang", + "name": "scala-compiler", + "version": "2.12.12", + "options": [ + "-deprecation" + ], + "jars": [ + "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-xml_2.12.jar", + "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-compiler.jar", + "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-library.jar", + "/home/fabio/.sbt/boot/scala-2.12.12/lib/jansi.jar", + "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-reflect.jar", + "/home/fabio/.sbt/boot/scala-2.12.12/lib/jline.jar" + ], + "analysis": "/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project/target/streams/compile/bloopAnalysisOut/_global/streams/inc_compile_2.12.zip", + "setup": { + "order": "mixed", + "addLibraryToBootClasspath": true, + "addCompilerToClasspath": false, + "addExtraJarsToClasspath": false, + "manageBootClasspath": true, + "filterLibraryFromClasspath": true + } + }, + "java": { + "options": [ + + ] + }, + "sbt": { + "sbtVersion": "1.4.4", + "autoImports": [ + "import _root_.scala.xml.{TopScope=>$scope}", + "import _root_.sbt._", + "import _root_.sbt.Keys._", + "import _root_.sbt.nio.Keys._", + "import _root_.sbt.ScriptedPlugin.autoImport._, _root_.sbt.plugins.MiniDependencyTreePlugin.autoImport._, _root_.sbtassembly.AssemblyPlugin.autoImport._, _root_.com.typesafe.sbt.SbtNativePackager.autoImport._, _root_.com.typesafe.sbt.packager.archetypes.JavaAppPackaging.autoImport._, _root_.com.typesafe.sbt.packager.archetypes.JavaServerAppPackaging.autoImport._, _root_.com.typesafe.sbt.packager.archetypes.jar.ClasspathJarPlugin.autoImport._, _root_.com.typesafe.sbt.packager.archetypes.jar.LauncherJarPlugin.autoImport._, _root_.com.typesafe.sbt.packager.archetypes.scripts.BashStartScriptPlugin.autoImport._, _root_.com.typesafe.sbt.packager.archetypes.scripts.BatStartScriptPlugin.autoImport._, _root_.com.typesafe.sbt.packager.archetypes.systemloader.SystemdPlugin.autoImport._, _root_.com.typesafe.sbt.packager.archetypes.systemloader.SystemloaderPlugin.autoImport._, _root_.com.typesafe.sbt.packager.debian.DebianPlugin.autoImport._, _root_.com.typesafe.sbt.packager.docker.DockerPlugin.autoImport._, _root_.com.typesafe.sbt.packager.graalvmnativeimage.GraalVMNativeImagePlugin.autoImport._, _root_.com.typesafe.sbt.packager.jdkpackager.JDKPackagerPlugin.autoImport._, _root_.com.typesafe.sbt.packager.linux.LinuxPlugin.autoImport._, _root_.com.typesafe.sbt.packager.rpm.RpmPlugin.autoImport._, _root_.com.typesafe.sbt.packager.universal.UniversalPlugin.autoImport._, _root_.com.typesafe.sbt.packager.windows.WindowsPlugin.autoImport._, _root_.sbtbuildinfo.BuildInfoPlugin.autoImport._", + "import _root_.sbt.plugins.IvyPlugin, _root_.sbt.plugins.JvmPlugin, _root_.sbt.plugins.CorePlugin, _root_.sbt.ScriptedPlugin, _root_.sbt.plugins.SbtPlugin, _root_.sbt.plugins.SemanticdbPlugin, _root_.sbt.plugins.JUnitXmlReportPlugin, _root_.sbt.plugins.Giter8TemplatePlugin, _root_.sbt.plugins.MiniDependencyTreePlugin, _root_.sbtassembly.AssemblyPlugin, _root_.com.typesafe.sbt.SbtNativePackager, _root_.com.typesafe.sbt.packager.archetypes.JavaAppPackaging, _root_.com.typesafe.sbt.packager.archetypes.JavaServerAppPackaging, _root_.com.typesafe.sbt.packager.archetypes.jar.ClasspathJarPlugin, _root_.com.typesafe.sbt.packager.archetypes.jar.LauncherJarPlugin, _root_.com.typesafe.sbt.packager.archetypes.scripts.AshScriptPlugin, _root_.com.typesafe.sbt.packager.archetypes.scripts.BashStartScriptPlugin, _root_.com.typesafe.sbt.packager.archetypes.scripts.BatStartScriptPlugin, _root_.com.typesafe.sbt.packager.archetypes.systemloader.SystemVPlugin, _root_.com.typesafe.sbt.packager.archetypes.systemloader.SystemdPlugin, _root_.com.typesafe.sbt.packager.archetypes.systemloader.SystemloaderPlugin, _root_.com.typesafe.sbt.packager.archetypes.systemloader.UpstartPlugin, _root_.com.typesafe.sbt.packager.debian.DebianDeployPlugin, _root_.com.typesafe.sbt.packager.debian.DebianPlugin, _root_.com.typesafe.sbt.packager.debian.JDebPackaging, _root_.com.typesafe.sbt.packager.docker.DockerPlugin, _root_.com.typesafe.sbt.packager.docker.DockerSpotifyClientPlugin, _root_.com.typesafe.sbt.packager.graalvmnativeimage.GraalVMNativeImagePlugin, _root_.com.typesafe.sbt.packager.jdkpackager.JDKPackagerDeployPlugin, _root_.com.typesafe.sbt.packager.jdkpackager.JDKPackagerPlugin, _root_.com.typesafe.sbt.packager.linux.LinuxPlugin, _root_.com.typesafe.sbt.packager.rpm.RpmDeployPlugin, _root_.com.typesafe.sbt.packager.rpm.RpmPlugin, _root_.com.typesafe.sbt.packager.universal.UniversalDeployPlugin, _root_.com.typesafe.sbt.packager.universal.UniversalPlugin, _root_.com.typesafe.sbt.packager.windows.WindowsDeployPlugin, _root_.com.typesafe.sbt.packager.windows.WindowsPlugin, _root_.sbtbuildinfo.BuildInfoPlugin" + ] + }, + "test": { + "frameworks": [ + { + "names": [ + "org.scalacheck.ScalaCheckFramework" + ] + }, + { + "names": [ + "org.specs2.runner.Specs2Framework", + "org.specs2.runner.SpecsFramework" + ] + }, + { + "names": [ + "org.specs.runner.SpecsFramework" + ] + }, + { + "names": [ + "org.scalatest.tools.Framework", + "org.scalatest.tools.ScalaTestFramework" + ] + }, + { + "names": [ + "com.novocode.junit.JUnitFramework" + ] + } + ], + "options": { + "excludes": [ + + ], + "arguments": [ + + ] + } + }, + "platform": { + "name": "jvm", + "config": { + "home": "/usr/lib/jvm/java-11-openjdk", + "options": [ + "-Duser.dir=/home/fabio/Documents/ETH/Bachelorarbeit/gobra_home/gobra/project" + ] + }, + "mainClass": [ + + ] + }, + "resolution": { + "modules": [ + { + "organization": "com.eed3si9n", + "name": "sbt-assembly", + "version": "0.14.8", + "configurations": "compile", + "artifacts": [ + { + "name": "sbt-assembly", + "path": "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.eed3si9n/sbt-assembly/scala_2.12/sbt_1.0/0.14.8/jars/sbt-assembly.jar" + } + ] + }, + { + "organization": "com.typesafe.sbt", + "name": "sbt-native-packager", + "version": "1.3.12", + "configurations": "compile", + "artifacts": [ + { + "name": "sbt-native-packager", + "path": "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.typesafe.sbt/sbt-native-packager/scala_2.12/sbt_1.0/1.3.12/jars/sbt-native-packager.jar" + }, + { + "name": "sbt-native-packager", + "classifier": "sources", + "path": "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.typesafe.sbt/sbt-native-packager/scala_2.12/sbt_1.0/1.3.12/srcs/sbt-native-packager-sources.jar" + }, + { + "name": "sbt-native-packager", + "classifier": "javadoc", + "path": "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.typesafe.sbt/sbt-native-packager/scala_2.12/sbt_1.0/1.3.12/docs/sbt-native-packager-javadoc.jar" + } + ] + }, + { + "organization": "com.eed3si9n", + "name": "sbt-buildinfo", + "version": "0.9.0", + "configurations": "compile", + "artifacts": [ + { + "name": "sbt-buildinfo", + "path": "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.eed3si9n/sbt-buildinfo/scala_2.12/sbt_1.0/0.9.0/jars/sbt-buildinfo.jar" + }, + { + "name": "sbt-buildinfo", + "classifier": "sources", + "path": "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.eed3si9n/sbt-buildinfo/scala_2.12/sbt_1.0/0.9.0/srcs/sbt-buildinfo-sources.jar" + }, + { + "name": "sbt-buildinfo", + "classifier": "javadoc", + "path": "/home/fabio/.cache/coursier/v1/https/repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.eed3si9n/sbt-buildinfo/scala_2.12/sbt_1.0/0.9.0/docs/sbt-buildinfo-javadoc.jar" + } + ] + }, + { + "organization": "org.scalactic", + "name": "scalactic_2.12", + "version": "3.0.1", + "configurations": "default", + "artifacts": [ + { + "name": "scalactic_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scalactic/scalactic_2.12/3.0.1/scalactic_2.12-3.0.1.jar" + } + ] + }, + { + "organization": "org.pantsbuild", + "name": "jarjar", + "version": "1.6.6", + "configurations": "default", + "artifacts": [ + { + "name": "jarjar", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/pantsbuild/jarjar/1.6.6/jarjar-1.6.6.jar" + } + ] + }, + { + "organization": "org.apache.commons", + "name": "commons-compress", + "version": "1.14", + "configurations": "default", + "artifacts": [ + { + "name": "commons-compress", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/commons/commons-compress/1.14/commons-compress-1.14.jar" + } + ] + }, + { + "organization": "org.apache.ant", + "name": "ant", + "version": "1.10.1", + "configurations": "default", + "artifacts": [ + { + "name": "ant", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/ant/ant/1.10.1/ant-1.10.1.jar" + } + ] + }, + { + "organization": "com.spotify", + "name": "docker-client", + "version": "8.9.0", + "configurations": "default", + "artifacts": [ + { + "name": "docker-client", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/spotify/docker-client/8.9.0/docker-client-8.9.0.jar" + } + ] + }, + { + "organization": "org.scala-lang", + "name": "scala-library", + "version": "2.12.12", + "configurations": "default", + "artifacts": [ + { + "name": "scala-library", + "path": "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-library.jar" + } + ] + }, + { + "organization": "org.scala-lang", + "name": "scala-reflect", + "version": "2.12.12", + "configurations": "default", + "artifacts": [ + { + "name": "scala-reflect", + "path": "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-reflect.jar" + } + ] + }, + { + "organization": "org.ow2.asm", + "name": "asm", + "version": "6.2", + "configurations": "default", + "artifacts": [ + { + "name": "asm", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm/6.2/asm-6.2.jar" + } + ] + }, + { + "organization": "org.ow2.asm", + "name": "asm-commons", + "version": "6.2", + "configurations": "default", + "artifacts": [ + { + "name": "asm-commons", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm-commons/6.2/asm-commons-6.2.jar" + } + ] + }, + { + "organization": "org.apache.maven", + "name": "maven-plugin-api", + "version": "3.3.9", + "configurations": "default", + "artifacts": [ + { + "name": "maven-plugin-api", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/maven/maven-plugin-api/3.3.9/maven-plugin-api-3.3.9.jar" + } + ] + }, + { + "organization": "org.apache.ant", + "name": "ant-launcher", + "version": "1.10.1", + "configurations": "default", + "artifacts": [ + { + "name": "ant-launcher", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/ant/ant-launcher/1.10.1/ant-launcher-1.10.1.jar" + } + ] + }, + { + "organization": "com.google.guava", + "name": "guava", + "version": "20.0", + "configurations": "default", + "artifacts": [ + { + "name": "guava", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/google/guava/guava/20.0/guava-20.0.jar" + } + ] + }, + { + "organization": "com.fasterxml.jackson.jaxrs", + "name": "jackson-jaxrs-json-provider", + "version": "2.8.8", + "configurations": "default", + "artifacts": [ + { + "name": "jackson-jaxrs-json-provider", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/jaxrs/jackson-jaxrs-json-provider/2.8.8/jackson-jaxrs-json-provider-2.8.8.jar" + } + ] + }, + { + "organization": "com.fasterxml.jackson.datatype", + "name": "jackson-datatype-guava", + "version": "2.8.8", + "configurations": "default", + "artifacts": [ + { + "name": "jackson-datatype-guava", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/datatype/jackson-datatype-guava/2.8.8/jackson-datatype-guava-2.8.8.jar" + } + ] + }, + { + "organization": "com.fasterxml.jackson.core", + "name": "jackson-databind", + "version": "2.8.8", + "configurations": "default", + "artifacts": [ + { + "name": "jackson-databind", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-databind/2.8.8/jackson-databind-2.8.8.jar" + } + ] + }, + { + "organization": "org.glassfish.jersey.core", + "name": "jersey-client", + "version": "2.22.2", + "configurations": "default", + "artifacts": [ + { + "name": "jersey-client", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/core/jersey-client/2.22.2/jersey-client-2.22.2.jar" + } + ] + }, + { + "organization": "org.glassfish.jersey.connectors", + "name": "jersey-apache-connector", + "version": "2.22.2", + "configurations": "default", + "artifacts": [ + { + "name": "jersey-apache-connector", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/connectors/jersey-apache-connector/2.22.2/jersey-apache-connector-2.22.2.jar" + } + ] + }, + { + "organization": "org.glassfish.jersey.media", + "name": "jersey-media-json-jackson", + "version": "2.22.2", + "configurations": "default", + "artifacts": [ + { + "name": "jersey-media-json-jackson", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/media/jersey-media-json-jackson/2.22.2/jersey-media-json-jackson-2.22.2.jar" + } + ] + }, + { + "organization": "commons-io", + "name": "commons-io", + "version": "2.5", + "configurations": "default", + "artifacts": [ + { + "name": "commons-io", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/commons-io/commons-io/2.5/commons-io-2.5.jar" + } + ] + }, + { + "organization": "org.apache.httpcomponents", + "name": "httpclient", + "version": "4.5", + "configurations": "default", + "artifacts": [ + { + "name": "httpclient", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/httpcomponents/httpclient/4.5/httpclient-4.5.jar" + } + ] + }, + { + "organization": "org.apache.httpcomponents", + "name": "httpcore", + "version": "4.4.5", + "configurations": "default", + "artifacts": [ + { + "name": "httpcore", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/httpcomponents/httpcore/4.4.5/httpcore-4.4.5.jar" + } + ] + }, + { + "organization": "com.github.jnr", + "name": "jnr-unixsocket", + "version": "0.8", + "configurations": "default", + "artifacts": [ + { + "name": "jnr-unixsocket", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-unixsocket/0.8/jnr-unixsocket-0.8.jar" + } + ] + }, + { + "organization": "commons-lang", + "name": "commons-lang", + "version": "2.6", + "configurations": "default", + "artifacts": [ + { + "name": "commons-lang", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/commons-lang/commons-lang/2.6/commons-lang-2.6.jar" + } + ] + }, + { + "organization": "org.bouncycastle", + "name": "bcpkix-jdk15on", + "version": "1.52", + "configurations": "default", + "artifacts": [ + { + "name": "bcpkix-jdk15on", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/bouncycastle/bcpkix-jdk15on/1.52/bcpkix-jdk15on-1.52.jar" + } + ] + }, + { + "organization": "ch.qos.logback", + "name": "logback-classic", + "version": "1.2.1", + "configurations": "default", + "artifacts": [ + { + "name": "logback-classic", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/ch/qos/logback/logback-classic/1.2.1/logback-classic-1.2.1.jar" + } + ] + }, + { + "organization": "org.ow2.asm", + "name": "asm-tree", + "version": "6.2", + "configurations": "default", + "artifacts": [ + { + "name": "asm-tree", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm-tree/6.2/asm-tree-6.2.jar" + } + ] + }, + { + "organization": "org.ow2.asm", + "name": "asm-analysis", + "version": "6.2", + "configurations": "default", + "artifacts": [ + { + "name": "asm-analysis", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm-analysis/6.2/asm-analysis-6.2.jar" + } + ] + }, + { + "organization": "org.apache.maven", + "name": "maven-model", + "version": "3.3.9", + "configurations": "default", + "artifacts": [ + { + "name": "maven-model", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/maven/maven-model/3.3.9/maven-model-3.3.9.jar" + } + ] + }, + { + "organization": "org.apache.maven", + "name": "maven-artifact", + "version": "3.3.9", + "configurations": "default", + "artifacts": [ + { + "name": "maven-artifact", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/maven/maven-artifact/3.3.9/maven-artifact-3.3.9.jar" + } + ] + }, + { + "organization": "org.eclipse.sisu", + "name": "org.eclipse.sisu.plexus", + "version": "0.3.2", + "configurations": "default", + "artifacts": [ + { + "name": "org.eclipse.sisu.plexus", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/eclipse/sisu/org.eclipse.sisu.plexus/0.3.2/org.eclipse.sisu.plexus-0.3.2.jar" + } + ] + }, + { + "organization": "com.fasterxml.jackson.jaxrs", + "name": "jackson-jaxrs-base", + "version": "2.8.8", + "configurations": "default", + "artifacts": [ + { + "name": "jackson-jaxrs-base", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/jaxrs/jackson-jaxrs-base/2.8.8/jackson-jaxrs-base-2.8.8.jar" + } + ] + }, + { + "organization": "com.fasterxml.jackson.core", + "name": "jackson-core", + "version": "2.8.8", + "configurations": "default", + "artifacts": [ + { + "name": "jackson-core", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-core/2.8.8/jackson-core-2.8.8.jar" + } + ] + }, + { + "organization": "com.fasterxml.jackson.module", + "name": "jackson-module-jaxb-annotations", + "version": "2.8.8", + "configurations": "default", + "artifacts": [ + { + "name": "jackson-module-jaxb-annotations", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/module/jackson-module-jaxb-annotations/2.8.8/jackson-module-jaxb-annotations-2.8.8.jar" + } + ] + }, + { + "organization": "com.fasterxml.jackson.core", + "name": "jackson-annotations", + "version": "2.8.0", + "configurations": "default", + "artifacts": [ + { + "name": "jackson-annotations", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-annotations/2.8.0/jackson-annotations-2.8.0.jar" + } + ] + }, + { + "organization": "javax.ws.rs", + "name": "javax.ws.rs-api", + "version": "2.0.1", + "configurations": "default", + "artifacts": [ + { + "name": "javax.ws.rs-api", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/ws/rs/javax.ws.rs-api/2.0.1/javax.ws.rs-api-2.0.1.jar" + } + ] + }, + { + "organization": "org.glassfish.jersey.core", + "name": "jersey-common", + "version": "2.22.2", + "configurations": "default", + "artifacts": [ + { + "name": "jersey-common", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/core/jersey-common/2.22.2/jersey-common-2.22.2.jar" + } + ] + }, + { + "organization": "org.glassfish.hk2", + "name": "hk2-api", + "version": "2.4.0-b34", + "configurations": "default", + "artifacts": [ + { + "name": "hk2-api", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/hk2-api/2.4.0-b34/hk2-api-2.4.0-b34.jar" + } + ] + }, + { + "organization": "org.glassfish.hk2.external", + "name": "javax.inject", + "version": "2.4.0-b34", + "configurations": "default", + "artifacts": [ + { + "name": "javax.inject", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/external/javax.inject/2.4.0-b34/javax.inject-2.4.0-b34.jar" + } + ] + }, + { + "organization": "org.glassfish.hk2", + "name": "hk2-locator", + "version": "2.4.0-b34", + "configurations": "default", + "artifacts": [ + { + "name": "hk2-locator", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/hk2-locator/2.4.0-b34/hk2-locator-2.4.0-b34.jar" + } + ] + }, + { + "organization": "org.glassfish.jersey.ext", + "name": "jersey-entity-filtering", + "version": "2.22.2", + "configurations": "default", + "artifacts": [ + { + "name": "jersey-entity-filtering", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/ext/jersey-entity-filtering/2.22.2/jersey-entity-filtering-2.22.2.jar" + } + ] + }, + { + "organization": "commons-logging", + "name": "commons-logging", + "version": "1.2", + "configurations": "default", + "artifacts": [ + { + "name": "commons-logging", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/commons-logging/commons-logging/1.2/commons-logging-1.2.jar" + } + ] + }, + { + "organization": "commons-codec", + "name": "commons-codec", + "version": "1.9", + "configurations": "default", + "artifacts": [ + { + "name": "commons-codec", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/commons-codec/commons-codec/1.9/commons-codec-1.9.jar" + } + ] + }, + { + "organization": "com.github.jnr", + "name": "jnr-ffi", + "version": "2.0.3", + "configurations": "default", + "artifacts": [ + { + "name": "jnr-ffi", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-ffi/2.0.3/jnr-ffi-2.0.3.jar" + } + ] + }, + { + "organization": "com.github.jnr", + "name": "jnr-constants", + "version": "0.8.7", + "configurations": "default", + "artifacts": [ + { + "name": "jnr-constants", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-constants/0.8.7/jnr-constants-0.8.7.jar" + } + ] + }, + { + "organization": "com.github.jnr", + "name": "jnr-enxio", + "version": "0.9", + "configurations": "default", + "artifacts": [ + { + "name": "jnr-enxio", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-enxio/0.9/jnr-enxio-0.9.jar" + } + ] + }, + { + "organization": "com.github.jnr", + "name": "jnr-posix", + "version": "3.0.12", + "configurations": "default", + "artifacts": [ + { + "name": "jnr-posix", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-posix/3.0.12/jnr-posix-3.0.12.jar" + } + ] + }, + { + "organization": "org.bouncycastle", + "name": "bcprov-jdk15on", + "version": "1.52", + "configurations": "default", + "artifacts": [ + { + "name": "bcprov-jdk15on", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/bouncycastle/bcprov-jdk15on/1.52/bcprov-jdk15on-1.52.jar" + } + ] + }, + { + "organization": "ch.qos.logback", + "name": "logback-core", + "version": "1.2.1", + "configurations": "default", + "artifacts": [ + { + "name": "logback-core", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/ch/qos/logback/logback-core/1.2.1/logback-core-1.2.1.jar" + } + ] + }, + { + "organization": "org.codehaus.plexus", + "name": "plexus-utils", + "version": "3.0.22", + "configurations": "default", + "artifacts": [ + { + "name": "plexus-utils", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/codehaus/plexus/plexus-utils/3.0.22/plexus-utils-3.0.22.jar" + } + ] + }, + { + "organization": "org.apache.commons", + "name": "commons-lang3", + "version": "3.4", + "configurations": "default", + "artifacts": [ + { + "name": "commons-lang3", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/commons/commons-lang3/3.4/commons-lang3-3.4.jar" + } + ] + }, + { + "organization": "javax.enterprise", + "name": "cdi-api", + "version": "1.0", + "configurations": "default", + "artifacts": [ + { + "name": "cdi-api", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/enterprise/cdi-api/1.0/cdi-api-1.0.jar" + } + ] + }, + { + "organization": "org.eclipse.sisu", + "name": "org.eclipse.sisu.inject", + "version": "0.3.2", + "configurations": "default", + "artifacts": [ + { + "name": "org.eclipse.sisu.inject", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/eclipse/sisu/org.eclipse.sisu.inject/0.3.2/org.eclipse.sisu.inject-0.3.2.jar" + } + ] + }, + { + "organization": "org.codehaus.plexus", + "name": "plexus-component-annotations", + "version": "1.5.5", + "configurations": "default", + "artifacts": [ + { + "name": "plexus-component-annotations", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/codehaus/plexus/plexus-component-annotations/1.5.5/plexus-component-annotations-1.5.5.jar" + } + ] + }, + { + "organization": "org.codehaus.plexus", + "name": "plexus-classworlds", + "version": "2.5.2", + "configurations": "default", + "artifacts": [ + { + "name": "plexus-classworlds", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/codehaus/plexus/plexus-classworlds/2.5.2/plexus-classworlds-2.5.2.jar" + } + ] + }, + { + "organization": "javax.annotation", + "name": "javax.annotation-api", + "version": "1.2", + "configurations": "default", + "artifacts": [ + { + "name": "javax.annotation-api", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/annotation/javax.annotation-api/1.2/javax.annotation-api-1.2.jar" + } + ] + }, + { + "organization": "org.glassfish.jersey.bundles.repackaged", + "name": "jersey-guava", + "version": "2.22.2", + "configurations": "default", + "artifacts": [ + { + "name": "jersey-guava", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/jersey/bundles/repackaged/jersey-guava/2.22.2/jersey-guava-2.22.2.jar" + } + ] + }, + { + "organization": "org.glassfish.hk2", + "name": "osgi-resource-locator", + "version": "1.0.1", + "configurations": "default", + "artifacts": [ + { + "name": "osgi-resource-locator", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/osgi-resource-locator/1.0.1/osgi-resource-locator-1.0.1.jar" + } + ] + }, + { + "organization": "org.glassfish.hk2", + "name": "hk2-utils", + "version": "2.4.0-b34", + "configurations": "default", + "artifacts": [ + { + "name": "hk2-utils", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/hk2-utils/2.4.0-b34/hk2-utils-2.4.0-b34.jar" + } + ] + }, + { + "organization": "org.glassfish.hk2.external", + "name": "aopalliance-repackaged", + "version": "2.4.0-b34", + "configurations": "default", + "artifacts": [ + { + "name": "aopalliance-repackaged", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/glassfish/hk2/external/aopalliance-repackaged/2.4.0-b34/aopalliance-repackaged-2.4.0-b34.jar" + } + ] + }, + { + "organization": "org.javassist", + "name": "javassist", + "version": "3.18.1-GA", + "configurations": "default", + "artifacts": [ + { + "name": "javassist", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/javassist/javassist/3.18.1-GA/javassist-3.18.1-GA.jar" + } + ] + }, + { + "organization": "com.github.jnr", + "name": "jffi", + "version": "1.2.9", + "configurations": "default", + "artifacts": [ + { + "name": "jffi", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jffi/1.2.9/jffi-1.2.9.jar" + } + ] + }, + { + "organization": "org.ow2.asm", + "name": "asm-util", + "version": "5.0.3", + "configurations": "default", + "artifacts": [ + { + "name": "asm-util", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/ow2/asm/asm-util/5.0.3/asm-util-5.0.3.jar" + } + ] + }, + { + "organization": "com.github.jnr", + "name": "jnr-x86asm", + "version": "1.0.2", + "configurations": "default", + "artifacts": [ + { + "name": "jnr-x86asm", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/jnr/jnr-x86asm/1.0.2/jnr-x86asm-1.0.2.jar" + } + ] + }, + { + "organization": "javax.annotation", + "name": "jsr250-api", + "version": "1.0", + "configurations": "default", + "artifacts": [ + { + "name": "jsr250-api", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/annotation/jsr250-api/1.0/jsr250-api-1.0.jar" + } + ] + }, + { + "organization": "javax.inject", + "name": "javax.inject", + "version": "1", + "configurations": "default", + "artifacts": [ + { + "name": "javax.inject", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/javax/inject/javax.inject/1/javax.inject-1.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "sbt", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "sbt", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/sbt/1.4.4/sbt-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "main_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "main_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/main_2.12/1.4.4/main_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "io_2.12", + "version": "1.4.0", + "configurations": "default", + "artifacts": [ + { + "name": "io_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/io_2.12/1.4.0/io_2.12-1.4.0.jar" + } + ] + }, + { + "organization": "org.scala-lang.modules", + "name": "scala-parser-combinators_2.12", + "version": "1.1.2", + "configurations": "default", + "artifacts": [ + { + "name": "scala-parser-combinators_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/modules/scala-parser-combinators_2.12/1.1.2/scala-parser-combinators_2.12-1.1.2.jar" + } + ] + }, + { + "organization": "org.scala-lang.modules", + "name": "scala-xml_2.12", + "version": "1.3.0", + "configurations": "default", + "artifacts": [ + { + "name": "scala-xml_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/modules/scala-xml_2.12/1.3.0/scala-xml_2.12-1.3.0.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "logic_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "logic_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/logic_2.12/1.4.4/logic_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "actions_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "actions_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/actions_2.12/1.4.4/actions_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "main-settings_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "main-settings_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/main-settings_2.12/1.4.4/main-settings_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "run_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "run_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/run_2.12/1.4.4/run_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "command_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "command_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/command_2.12/1.4.4/command_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "collections_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "collections_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/collections_2.12/1.4.4/collections_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "scripted-plugin_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "scripted-plugin_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/scripted-plugin_2.12/1.4.4/scripted-plugin_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc-lm-integration_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "zinc-lm-integration_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-lm-integration_2.12/1.4.4/zinc-lm-integration_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "util-logging_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "util-logging_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-logging_2.12/1.4.4/util-logging_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "launcher-interface", + "version": "1.1.5", + "configurations": "default", + "artifacts": [ + { + "name": "launcher-interface", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/launcher-interface/1.1.5/launcher-interface-1.1.5.jar" + } + ] + }, + { + "organization": "com.github.ben-manes.caffeine", + "name": "caffeine", + "version": "2.8.5", + "configurations": "default", + "artifacts": [ + { + "name": "caffeine", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/github/ben-manes/caffeine/caffeine/2.8.5/caffeine-2.8.5.jar" + } + ] + }, + { + "organization": "io.get-coursier", + "name": "lm-coursier-shaded_2.12", + "version": "2.0.3", + "configurations": "default", + "artifacts": [ + { + "name": "lm-coursier-shaded_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/io/get-coursier/lm-coursier-shaded_2.12/2.0.3/lm-coursier-shaded_2.12-2.0.3.jar" + } + ] + }, + { + "organization": "org.apache.logging.log4j", + "name": "log4j-api", + "version": "2.11.2", + "configurations": "default", + "artifacts": [ + { + "name": "log4j-api", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/logging/log4j/log4j-api/2.11.2/log4j-api-2.11.2.jar" + } + ] + }, + { + "organization": "org.apache.logging.log4j", + "name": "log4j-core", + "version": "2.11.2", + "configurations": "default", + "artifacts": [ + { + "name": "log4j-core", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/logging/log4j/log4j-core/2.11.2/log4j-core-2.11.2.jar" + } + ] + }, + { + "organization": "org.apache.logging.log4j", + "name": "log4j-slf4j-impl", + "version": "2.11.2", + "configurations": "default", + "artifacts": [ + { + "name": "log4j-slf4j-impl", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/apache/logging/log4j/log4j-slf4j-impl/2.11.2/log4j-slf4j-impl-2.11.2.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "librarymanagement-core_2.12", + "version": "1.4.1", + "configurations": "default", + "artifacts": [ + { + "name": "librarymanagement-core_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/librarymanagement-core_2.12/1.4.1/librarymanagement-core_2.12-1.4.1.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "librarymanagement-ivy_2.12", + "version": "1.4.1", + "configurations": "default", + "artifacts": [ + { + "name": "librarymanagement-ivy_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/librarymanagement-ivy_2.12/1.4.1/librarymanagement-ivy_2.12-1.4.1.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "compiler-interface", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "compiler-interface", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/compiler-interface/1.4.3/compiler-interface-1.4.3.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc-compile_2.12", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "zinc-compile_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-compile_2.12/1.4.3/zinc-compile_2.12-1.4.3.jar" + } + ] + }, + { + "organization": "com.swoval", + "name": "file-tree-views", + "version": "2.1.4", + "configurations": "default", + "artifacts": [ + { + "name": "file-tree-views", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/swoval/file-tree-views/2.1.4/file-tree-views-2.1.4.jar" + } + ] + }, + { + "organization": "net.java.dev.jna", + "name": "jna", + "version": "5.5.0", + "configurations": "default", + "artifacts": [ + { + "name": "jna", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/net/java/dev/jna/jna/5.5.0/jna-5.5.0.jar" + } + ] + }, + { + "organization": "net.java.dev.jna", + "name": "jna-platform", + "version": "5.5.0", + "configurations": "default", + "artifacts": [ + { + "name": "jna-platform", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/net/java/dev/jna/jna-platform/5.5.0/jna-platform-5.5.0.jar" + } + ] + }, + { + "organization": "org.slf4j", + "name": "slf4j-api", + "version": "1.7.26", + "configurations": "default", + "artifacts": [ + { + "name": "slf4j-api", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/slf4j/slf4j-api/1.7.26/slf4j-api-1.7.26.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "util-relation_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "util-relation_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-relation_2.12/1.4.4/util-relation_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "completion_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "completion_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/completion_2.12/1.4.4/completion_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "task-system_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "task-system_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/task-system_2.12/1.4.4/task-system_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "tasks_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "tasks_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/tasks_2.12/1.4.4/tasks_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "testing_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "testing_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/testing_2.12/1.4.4/testing_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "util-tracking_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "util-tracking_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-tracking_2.12/1.4.4/util-tracking_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "com.eed3si9n", + "name": "sjson-new-scalajson_2.12", + "version": "0.9.1", + "configurations": "default", + "artifacts": [ + { + "name": "sjson-new-scalajson_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/sjson-new-scalajson_2.12/0.9.1/sjson-new-scalajson_2.12-0.9.1.jar" + } + ] + }, + { + "organization": "org.scala-sbt.jline3", + "name": "jline-terminal", + "version": "3.16.0-sbt-211a082ed6326908dc84ca017ce4430728f18a8a", + "configurations": "default", + "artifacts": [ + { + "name": "jline-terminal", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/jline3/jline-terminal/3.16.0-sbt-211a082ed6326908dc84ca017ce4430728f18a8a/jline-terminal-3.16.0-sbt-211a082ed6326908dc84ca017ce4430728f18a8a.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc-classpath_2.12", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "zinc-classpath_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-classpath_2.12/1.4.3/zinc-classpath_2.12-1.4.3.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc-apiinfo_2.12", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "zinc-apiinfo_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-apiinfo_2.12/1.4.3/zinc-apiinfo_2.12-1.4.3.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc_2.12", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "zinc_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc_2.12/1.4.3/zinc_2.12-1.4.3.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "core-macros_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "core-macros_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/core-macros_2.12/1.4.4/core-macros_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "util-cache_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "util-cache_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-cache_2.12/1.4.4/util-cache_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "util-control_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "util-control_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-control_2.12/1.4.4/util-control_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "protocol_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "protocol_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/protocol_2.12/1.4.4/protocol_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "com.eed3si9n", + "name": "sjson-new-core_2.12", + "version": "0.9.1", + "configurations": "default", + "artifacts": [ + { + "name": "sjson-new-core_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/sjson-new-core_2.12/0.9.1/sjson-new-core_2.12-0.9.1.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "template-resolver", + "version": "0.1", + "configurations": "default", + "artifacts": [ + { + "name": "template-resolver", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/template-resolver/0.1/template-resolver-0.1.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "util-position_2.12", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "util-position_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-position_2.12/1.4.4/util-position_2.12-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc-compile-core_2.12", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "zinc-compile-core_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-compile-core_2.12/1.4.3/zinc-compile-core_2.12-1.4.3.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "util-interface", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "util-interface", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/util-interface/1.4.4/util-interface-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt.jline", + "name": "jline", + "version": "2.14.7-sbt-5e51b9d4f9631ebfa29753ce4accc57808e7fd6b", + "configurations": "default", + "artifacts": [ + { + "name": "jline", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/jline/jline/2.14.7-sbt-5e51b9d4f9631ebfa29753ce4accc57808e7fd6b/jline-2.14.7-sbt-5e51b9d4f9631ebfa29753ce4accc57808e7fd6b.jar" + } + ] + }, + { + "organization": "org.jline", + "name": "jline-terminal-jna", + "version": "3.16.0", + "configurations": "default", + "artifacts": [ + { + "name": "jline-terminal-jna", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-terminal-jna/3.16.0/jline-terminal-jna-3.16.0.jar" + } + ] + }, + { + "organization": "org.jline", + "name": "jline-terminal-jansi", + "version": "3.16.0", + "configurations": "default", + "artifacts": [ + { + "name": "jline-terminal-jansi", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-terminal-jansi/3.16.0/jline-terminal-jansi-3.16.0.jar" + } + ] + }, + { + "organization": "com.lmax", + "name": "disruptor", + "version": "3.4.2", + "configurations": "default", + "artifacts": [ + { + "name": "disruptor", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/lmax/disruptor/3.4.2/disruptor-3.4.2.jar" + } + ] + }, + { + "organization": "org.checkerframework", + "name": "checker-qual", + "version": "3.4.1", + "configurations": "default", + "artifacts": [ + { + "name": "checker-qual", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/checkerframework/checker-qual/3.4.1/checker-qual-3.4.1.jar" + } + ] + }, + { + "organization": "com.google.errorprone", + "name": "error_prone_annotations", + "version": "2.4.0", + "configurations": "default", + "artifacts": [ + { + "name": "error_prone_annotations", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/google/errorprone/error_prone_annotations/2.4.0/error_prone_annotations-2.4.0.jar" + } + ] + }, + { + "organization": "org.scala-lang.modules", + "name": "scala-collection-compat_2.12", + "version": "2.2.0", + "configurations": "default", + "artifacts": [ + { + "name": "scala-collection-compat_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/modules/scala-collection-compat_2.12/2.2.0/scala-collection-compat_2.12-2.2.0.jar" + } + ] + }, + { + "organization": "org.scala-lang", + "name": "scala-compiler", + "version": "2.12.12", + "configurations": "default", + "artifacts": [ + { + "name": "scala-compiler", + "path": "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-compiler.jar" + } + ] + }, + { + "organization": "com.jcraft", + "name": "jsch", + "version": "0.1.54", + "configurations": "default", + "artifacts": [ + { + "name": "jsch", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/jcraft/jsch/0.1.54/jsch-0.1.54.jar" + } + ] + }, + { + "organization": "com.eed3si9n", + "name": "gigahorse-okhttp_2.12", + "version": "0.5.0", + "configurations": "default", + "artifacts": [ + { + "name": "gigahorse-okhttp_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/gigahorse-okhttp_2.12/0.5.0/gigahorse-okhttp_2.12-0.5.0.jar" + } + ] + }, + { + "organization": "com.squareup.okhttp3", + "name": "okhttp-urlconnection", + "version": "3.7.0", + "configurations": "default", + "artifacts": [ + { + "name": "okhttp-urlconnection", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/squareup/okhttp3/okhttp-urlconnection/3.7.0/okhttp-urlconnection-3.7.0.jar" + } + ] + }, + { + "organization": "org.scala-sbt.ivy", + "name": "ivy", + "version": "2.3.0-sbt-fbc4f586aeeb1591710b14eb4f41b94880dcd745", + "configurations": "default", + "artifacts": [ + { + "name": "ivy", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/ivy/ivy/2.3.0-sbt-fbc4f586aeeb1591710b14eb4f41b94880dcd745/ivy-2.3.0-sbt-fbc4f586aeeb1591710b14eb4f41b94880dcd745.jar" + } + ] + }, + { + "organization": "org.jline", + "name": "jline-reader", + "version": "3.16.0", + "configurations": "default", + "artifacts": [ + { + "name": "jline-reader", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-reader/3.16.0/jline-reader-3.16.0.jar" + } + ] + }, + { + "organization": "org.jline", + "name": "jline-builtins", + "version": "3.16.0", + "configurations": "default", + "artifacts": [ + { + "name": "jline-builtins", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-builtins/3.16.0/jline-builtins-3.16.0.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "test-agent", + "version": "1.4.4", + "configurations": "default", + "artifacts": [ + { + "name": "test-agent", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/test-agent/1.4.4/test-agent-1.4.4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "test-interface", + "version": "1.0", + "configurations": "default", + "artifacts": [ + { + "name": "test-interface", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/test-interface/1.0/test-interface-1.0.jar" + } + ] + }, + { + "organization": "com.eed3si9n", + "name": "shaded-jawn-parser_2.12", + "version": "0.9.1", + "configurations": "default", + "artifacts": [ + { + "name": "shaded-jawn-parser_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/shaded-jawn-parser_2.12/0.9.1/shaded-jawn-parser_2.12-0.9.1.jar" + } + ] + }, + { + "organization": "com.eed3si9n", + "name": "shaded-scalajson_2.12", + "version": "1.0.0-M4", + "configurations": "default", + "artifacts": [ + { + "name": "shaded-scalajson_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/shaded-scalajson_2.12/1.0.0-M4/shaded-scalajson_2.12-1.0.0-M4.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "compiler-bridge_2.12", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "compiler-bridge_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/compiler-bridge_2.12/1.4.3/compiler-bridge_2.12-1.4.3.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc-classfile_2.12", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "zinc-classfile_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-classfile_2.12/1.4.3/zinc-classfile_2.12-1.4.3.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc-core_2.12", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "zinc-core_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-core_2.12/1.4.3/zinc-core_2.12-1.4.3.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc-persist_2.12", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "zinc-persist_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-persist_2.12/1.4.3/zinc-persist_2.12-1.4.3.jar" + } + ] + }, + { + "organization": "com.eed3si9n", + "name": "sjson-new-murmurhash_2.12", + "version": "0.9.1", + "configurations": "default", + "artifacts": [ + { + "name": "sjson-new-murmurhash_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/sjson-new-murmurhash_2.12/0.9.1/sjson-new-murmurhash_2.12-0.9.1.jar" + } + ] + }, + { + "organization": "org.scala-sbt.ipcsocket", + "name": "ipcsocket", + "version": "1.1.0", + "configurations": "default", + "artifacts": [ + { + "name": "ipcsocket", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/ipcsocket/ipcsocket/1.1.0/ipcsocket-1.1.0.jar" + } + ] + }, + { + "organization": "net.openhft", + "name": "zero-allocation-hashing", + "version": "0.10.1", + "configurations": "default", + "artifacts": [ + { + "name": "zero-allocation-hashing", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/net/openhft/zero-allocation-hashing/0.10.1/zero-allocation-hashing-0.10.1.jar" + } + ] + }, + { + "organization": "org.fusesource.jansi", + "name": "jansi", + "version": "1.18", + "configurations": "default", + "artifacts": [ + { + "name": "jansi", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/fusesource/jansi/jansi/1.18/jansi-1.18.jar" + } + ] + }, + { + "organization": "org.jline", + "name": "jline-terminal", + "version": "3.16.0", + "configurations": "default", + "artifacts": [ + { + "name": "jline-terminal", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-terminal/3.16.0/jline-terminal-3.16.0.jar" + } + ] + }, + { + "organization": "com.eed3si9n", + "name": "gigahorse-core_2.12", + "version": "0.5.0", + "configurations": "default", + "artifacts": [ + { + "name": "gigahorse-core_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/eed3si9n/gigahorse-core_2.12/0.5.0/gigahorse-core_2.12-0.5.0.jar" + } + ] + }, + { + "organization": "com.squareup.okhttp3", + "name": "okhttp", + "version": "3.14.2", + "configurations": "default", + "artifacts": [ + { + "name": "okhttp", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/squareup/okhttp3/okhttp/3.14.2/okhttp-3.14.2.jar" + } + ] + }, + { + "organization": "org.jline", + "name": "jline-style", + "version": "3.16.0", + "configurations": "default", + "artifacts": [ + { + "name": "jline-style", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/jline/jline-style/3.16.0/jline-style-3.16.0.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "zinc-persist-core-assembly", + "version": "1.4.3", + "configurations": "default", + "artifacts": [ + { + "name": "zinc-persist-core-assembly", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/zinc-persist-core-assembly/1.4.3/zinc-persist-core-assembly-1.4.3.jar" + } + ] + }, + { + "organization": "org.scala-sbt", + "name": "sbinary_2.12", + "version": "0.5.1", + "configurations": "default", + "artifacts": [ + { + "name": "sbinary_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-sbt/sbinary_2.12/0.5.1/sbinary_2.12-0.5.1.jar" + } + ] + }, + { + "organization": "com.typesafe", + "name": "ssl-config-core_2.12", + "version": "0.4.0", + "configurations": "default", + "artifacts": [ + { + "name": "ssl-config-core_2.12", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/typesafe/ssl-config-core_2.12/0.4.0/ssl-config-core_2.12-0.4.0.jar" + } + ] + }, + { + "organization": "org.reactivestreams", + "name": "reactive-streams", + "version": "1.0.2", + "configurations": "default", + "artifacts": [ + { + "name": "reactive-streams", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/org/reactivestreams/reactive-streams/1.0.2/reactive-streams-1.0.2.jar" + } + ] + }, + { + "organization": "com.squareup.okio", + "name": "okio", + "version": "1.17.2", + "configurations": "default", + "artifacts": [ + { + "name": "okio", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/squareup/okio/okio/1.17.2/okio-1.17.2.jar" + } + ] + }, + { + "organization": "com.typesafe", + "name": "config", + "version": "1.3.3", + "configurations": "default", + "artifacts": [ + { + "name": "config", + "path": "/home/fabio/.cache/coursier/v1/https/repo1.maven.org/maven2/com/typesafe/config/1.3.3/config-1.3.3.jar" + } + ] + }, + { + "organization": "org.scala-lang", + "name": "scala-compiler", + "version": "2.12.12", + "configurations": "optional", + "artifacts": [ + { + "name": "scala-compiler", + "path": "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-compiler.jar" + } + ] + }, + { + "organization": "org.scala-lang", + "name": "scala-library", + "version": "2.12.12", + "configurations": "optional", + "artifacts": [ + { + "name": "scala-library", + "path": "/home/fabio/.sbt/boot/scala-2.12.12/lib/scala-library.jar" + } + ] + } + ] + }, + "tags": [ + "library" + ] + } +} \ No newline at end of file diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index aedc1fa22..4f8db8c93 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/src/main/scala/viper/gobra/Gobra.scala @@ -14,6 +14,7 @@ import viper.gobra.ast.frontend.PPackage import viper.gobra.ast.internal.Program import viper.gobra.ast.internal.transform.OverflowChecksTransform import viper.gobra.backend.BackendVerifier +import viper.gobra.reporting.BackTranslator.VerificationBackTrackInfo import viper.gobra.frontend.info.{Info, TypeInfo} import viper.gobra.frontend.{Config, Desugar, Parser, ScallopGobraConfig} import viper.gobra.reporting.{AppliedInternalTransformsMessage, BackTranslator, CopyrightReport, VerifierError, VerifierResult} @@ -77,8 +78,20 @@ class Gobra extends GoVerifier with GoIdeVerifier { typeInfo <- performTypeChecking(parsedPackage, finalConfig) program <- performDesugaring(parsedPackage, typeInfo, finalConfig) program <- performInternalTransformations(program, finalConfig) - viperTask <- performViperEncoding(program, finalConfig) - } yield (viperTask, finalConfig) + programWithBackInfo <- performViperEncoding(program, finalConfig,typeInfo) + + (encodedProgram, encodingBackInfo) = (programWithBackInfo.program,programWithBackInfo.backtrack) + task = BackendVerifier.Task( + encodedProgram, + BackTranslator.BackTrackInfo( + encodingBackInfo.errorT, + encodingBackInfo.reasonT, + encodedProgram, + typeInfo, + config + ) + ) + } yield (task, finalConfig) } task.flatMap{ @@ -183,9 +196,9 @@ class Gobra extends GoVerifier with GoIdeVerifier { } } - private def performViperEncoding(program: Program, config: Config): Either[Vector[VerifierError], BackendVerifier.Task] = { + private def performViperEncoding(program: Program, config: Config,typeInfo:viper.gobra.frontend.info.TypeInfo): Either[Vector[VerifierError], BackendVerifier.Task] = { if (config.shouldViperEncode) { - Right(Translator.translate(program)(config)) + Right(Translator.translate(program)(config,typeInfo)) } else { Left(Vector()) } diff --git a/src/main/scala/viper/gobra/backend/BackendVerifier.scala b/src/main/scala/viper/gobra/backend/BackendVerifier.scala index bbc09a007..849a38a01 100644 --- a/src/main/scala/viper/gobra/backend/BackendVerifier.scala +++ b/src/main/scala/viper/gobra/backend/BackendVerifier.scala @@ -41,6 +41,10 @@ object BackendVerifier { case _ => } + if(config.counterexample.isDefined){ + exePaths ++= Vector("--counterexample", "mapped") + } + (config.backend, config.boogieExe) match { case (Carbon, Some(boogieExe)) => exePaths ++= Vector("--boogieExe", boogieExe) diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala index 5cc2f3549..18e1596ac 100644 --- a/src/main/scala/viper/gobra/backend/ViperBackends.scala +++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala @@ -16,10 +16,12 @@ object ViperBackends { def create(exePaths: Vector[String]): Silicon = { var options: Vector[String] = Vector.empty + options ++= Vector("--logLevel", "ERROR") options ++= Vector("--disableCatchingExceptions") options ++= Vector("--enableMoreCompleteExhale") options ++= exePaths + new Silicon(options) } diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 8d282fbf4..828c1b53f 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -17,8 +17,10 @@ import org.slf4j.LoggerFactory import viper.gobra.backend.{ViperBackend, ViperBackends, ViperVerifierConfig} import viper.gobra.GoVerifier import viper.gobra.frontend.PackageResolver.{FileResource, RegularImport} -import viper.gobra.reporting.{FileWriterReporter, GobraReporter, StdIOReporter} +import viper.gobra.reporting.{FileWriterReporter, GobraReporter, StdIOReporter,CounterexampleConfigs} import viper.gobra.util.{TypeBounds, Violation} +import org.scalactic.Bool +import _root_.viper.gobra.reporting.CounterexampleConfig object LoggerDefaults { @@ -41,10 +43,12 @@ case class Config( checkOverflows: Boolean = false, checkConsistency: Boolean = false, shouldVerify: Boolean = true, + // The go language specification states that int and uint variables can have either 32bit or 64, as long // as they have the same size. This flag allows users to pick the size of int's and uints's: 32 if true, // 64 bit otherwise. - int32bit: Boolean = false + int32bit: Boolean = false, + counterexample :Option[CounterexampleConfig] = None ) { def merge(other: Config): Config = { // this config takes precedence over other config @@ -63,7 +67,8 @@ case class Config( shouldViperEncode = shouldViperEncode, checkOverflows = checkOverflows || other.checkOverflows, shouldVerify = shouldVerify, - int32bit = int32bit || other.int32bit + int32bit = int32bit || other.int32bit, + counterexample=counterexample ) } @@ -207,6 +212,20 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals noshort = false ) + val counterexample:ScallopOption[CounterexampleConfig] = opt[CounterexampleConfig]( + name = "counterexample", + descr = "Adds counterexamples to output can be run with: mapped, native, reduced, extended (default: no counterexample)" + +"curently works witch SILICON as a backend", + default = None, + noshort = false + )(singleArgConverter({ + case "mapped" => CounterexampleConfigs.MappedCounterexamples + case "native" => CounterexampleConfigs.NativeCounterexamples + case "reduced" => CounterexampleConfigs.ReducedCounterexamples + case "extended" => CounterexampleConfigs.ExtendedCounterexamples + case _ => CounterexampleConfigs.MappedCounterexamples + })) + /** * Exception handling @@ -379,6 +398,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals shouldViperEncode = shouldViperEncode, checkOverflows = checkOverflows(), int32bit = int32Bit(), - shouldVerify = shouldVerify + shouldVerify = shouldVerify, + counterexample=counterexample.toOption ) } diff --git a/src/main/scala/viper/gobra/reporting/BackTranslator.scala b/src/main/scala/viper/gobra/reporting/BackTranslator.scala index 7b4d3f32f..b343574df 100644 --- a/src/main/scala/viper/gobra/reporting/BackTranslator.scala +++ b/src/main/scala/viper/gobra/reporting/BackTranslator.scala @@ -5,10 +5,13 @@ // Copyright (c) 2011-2020 ETH Zurich. package viper.gobra.reporting +import viper.gobra.ast.frontend._ +import viper.gobra.frontend.info.TypeInfo import viper.gobra.backend.BackendVerifier -import viper.gobra.frontend.Config +import viper.gobra.frontend.{Config,Parser} import viper.silver.{ast => vpr} import viper.silver +import java.nio.file.{Path,Paths} import scala.annotation.unused @@ -18,20 +21,27 @@ object BackTranslator { def translate(error: silver.verifier.VerificationError): VerificationError def translate(reason: silver.verifier.ErrorReason): VerificationErrorReason } - - case class BackTrackInfo( + case class VerificationBackTrackInfo( errorT: Seq[BackTranslator.ErrorTransformer], reasonT: Seq[BackTranslator.ReasonTransformer] ) + case class BackTrackInfo( + errorT: Seq[BackTranslator.ErrorTransformer], + reasonT: Seq[BackTranslator.ReasonTransformer], + viperprogram:vpr.Program, + typeInfo:TypeInfo, + config:Config + ) type ErrorTransformer = PartialFunction[silver.verifier.VerificationError, VerificationError] type ReasonTransformer = PartialFunction[silver.verifier.ErrorReason, VerificationErrorReason] - def backTranslate(result: BackendVerifier.Result)(@unused config: Config): VerifierResult = result match { + def backTranslate(result: BackendVerifier.Result)(/* @unused */ config: Config): VerifierResult = + result match { case BackendVerifier.Success => VerifierResult.Success - case BackendVerifier.Failure(errors, backtrack) => - val errorTranslator = new DefaultErrorBackTranslator(backtrack) - VerifierResult.Failure(errors map errorTranslator.translate) + case BackendVerifier.Failure(errors, backtrack) => + val errorTranslator = new DefaultErrorBackTranslator(backtrack.copy(config=config)) //TODO make this more clean e.g. remove config from backtrack Info + VerifierResult.Failure(errors map errorTranslator.translate) } implicit class RichErrorMessage(error: silver.verifier.ErrorMessage) { diff --git a/src/main/scala/viper/gobra/reporting/CounterexampleBackTranslator.scala b/src/main/scala/viper/gobra/reporting/CounterexampleBackTranslator.scala new file mode 100644 index 000000000..e8aa12e67 --- /dev/null +++ b/src/main/scala/viper/gobra/reporting/CounterexampleBackTranslator.scala @@ -0,0 +1,507 @@ +package viper.gobra.reporting + +import viper.gobra.translator.interfaces.Context +import viper.gobra.ast.frontend._ +import viper.gobra.reporting._ +import viper.gobra.frontend.{Config,Parser} +import viper.silicon.interfaces.SiliconMappedCounterexample +import viper.silver +import viper.silver.{ast=> vpr} +import viper.silver.ast.{LineColumnPosition, SourcePosition} +import viper.silicon.{reporting=> sil} +import viper.gobra.frontend.info.base.{SymbolTable} +import viper.gobra.frontend.info.base.Type._ +import viper.gobra.frontend.info.TypeInfo +//import viper.gobra.internal.utility.Nodes +import viper.silver.verifier.{Counterexample,Model} + + + + +trait CounterexampleConfig +/** + * simple counterexample distinction this is obsolete but kept to run the counterexamples on the config + */ +object CounterexampleConfigs{ + object MappedCounterexamples extends CounterexampleConfig + object NativeCounterexamples extends CounterexampleConfig + object ReducedCounterexamples extends CounterexampleConfig + object ExtendedCounterexamples extends CounterexampleConfig +} + +case class CounterexampleBackTranslator(backtrack: BackTranslator.BackTrackInfo){ + def translate(counterexample: silver.verifier.Counterexample, error: PNode): Option[GobraCounterexample] = { + val typeinfo = backtrack.typeInfo + InterpreterCache.setTypeInfo(typeinfo) + val converter: sil.Converter = counterexample match { + case c: SiliconMappedCounterexample => c.converter + case _ => return None + } + val viperModel : Map[String,sil.ExtractedModel] = converter.modelAtLabel ++ Seq(("return",converter.extractedModel)) + val fi = viperModel.keys.head + val viperVars : Seq[String] = viperModel.apply(fi).entries.keys.toSeq + val viperProgram = backtrack.viperprogram + //all variable declarations of the viper program, issue: if two vipervariables have the same name we cannot distinguish (we have to assume they are unique) + val varDeclNodes = viperProgram.collect(x => if(x.isInstanceOf[vpr.LocalVarDecl] && viperVars.contains(x.asInstanceOf[vpr.LocalVarDecl].name)) Some(x.asInstanceOf[vpr.LocalVarDecl]) else None).collect({case Some(x)=> x}) + //val labels = viperProgram.collect({case x:vpr.Label => x}) + //map from viper declarations to entries + val declarationMap : Map[String,Map[vpr.LocalVarDecl, sil.ExtractedModelEntry]] = viperModel.map(y => (y._1, varDeclNodes.map(x => (x,y._2.entries.apply(x.name))).toMap)) + + val predicates : Seq[vpr.Predicate] =viperProgram.collect(x=> x match {case p:vpr.Predicate =>p}).toSeq + InterpreterCache.setPredicates(predicates) + + val gobraPredicates :Seq[PFPredicateDecl] = predicates.map(Source.unapply(_) match{case Some(t)=> Some(t.pnode); case _=> None}).collect(x=> x match{case Some(p)=> p}).collect(x=> x match{case p:PFPredicateDecl=>p}) + InterpreterCache.setGobraPredicates(gobraPredicates) + + //map from info to counterexample entry + val declInfosMap: Map[String,Map[Source.Verifier.Info,sil.ExtractedModelEntry]] = declarationMap.map(y=>(y._1,y._2.map(x=>(Source.unapply(x._1) match {case Some(t) => (t,x._2) })))) + + val tranlator = MasterInterpreter(converter).interpret(_,_) + //translate the values + //printf(s"${converter.extractedHeap}\n---${converter.store}") + val translated = declInfosMap.map(y=>(y._1,y._2.map(x=> + {InterpreterCache.clearCache(); + val typeval = Util.getType(x._1.pnode,typeinfo) + //printf(s"$x;;$typeval\n") + (x._1,tranlator(x._2,typeval)) + } + ))) + //the pnode does not always correspond to the same node possible (filter for which the pnode is not a substrong of the node) + lazy val glabelModel = new GobraModelAtLabel(translated.map(y=>(y._1,new GobraModel(y._2.filterNot(x=>isUnnecessary(x._1) ).map(x=>((x._1,x._1.node.toString),x._2)))))) + //printf(s"${converter.domains}\n${converter.non_domain_functions}") + InterpreterCache.clearPreds() + InterpreterCache.clearGobraPreds() + lazy val ret = Some(new GobraCounterexample(glabelModel)) + backtrack.config.counterexample match { + case Some(CounterexampleConfigs.NativeCounterexamples) => Some(new GobraNativeCounterexample(counterexample.asInstanceOf[SiliconMappedCounterexample])) + //TODO get error + case Some(CounterexampleConfigs.ReducedCounterexamples) => Some(new ReducedCounterexample(glabelModel,error)) + case _ => ret + } + + } + def isUnnecessary(info: Source.Verifier.Info): Boolean = { + //Embeddings and such //usually for multi variable assgnent //function calls // parameter and return values (ISSUE sometimes we want both TODO: on return label use result param and in old label use input params) + info.node.toString.contains("$") || info.pnode.toString.contains("=") || info.pnode.toString.contains("(") || info.pnode.toString.contains("{")//|| info.pnode.toString.contains(" ") + } +} +object Util{ + def getType(pnode: PNode, info: viper.gobra.frontend.info.ExternalTypeInfo): Type = { + pnode match { + case (x: PIdnNode) => info.typ(x) + case (x: PParameter) => info.typ(x) + case (x: PExpression) => info.typ(x) + case (x: PMisc) => info.typ(x) + case _ => UnknownType + } + } + def getDefault(t: Type): GobraModelEntry = { + t match { + case _: IntT => LitIntEntry(0) + case BooleanT => LitBoolEntry(false) + case _: PointerT => LitNilEntry() + case a: ArrayT => LitArrayEntry(a,Seq()) + case OptionT(elem) => LitOptionEntry(None) + case s: StructT => LitStructEntry(s,s.fields.map(x=>(x._1,getDefault(x._2).asInstanceOf[LitEntry]))) + case StringT => LitStringEntry("") + case _ => LitNilEntry() + } + } + //prints the values with the correct indentations for the commandline + def prettyPrint(input: GobraModelEntry, level: Int): String = { + val indent = "\t\t\t" ++ "\t".repeat(level) + val postdent = "\t\t" ++ "\t".repeat(level) + val predent = "\t\t"++"\t".repeat(level) + input match { + case LitStructEntry(_, m) => { + if(m.isEmpty){ + "struct{}" + }else{ + val sub = m.map(x=>(x._1,prettyPrint(x._2,level+1))) + s"struct{\n${sub.map(x=>s"$indent${x._1}=${x._2}").mkString(";\n")}\n${postdent}}" + } + } + case LitDeclaredEntry(name, value) => { + value match { + case LitStructEntry(_,_) => prettyPrint(value,level).replaceFirst("struct",name) + case LitAdressedEntry(value, address,perm) => prettyPrint(LitDeclaredEntry(name,value),level) ++ s"@$address," /* (${perm.getOrElse("?")})" */ + case u: UserDomainEntry => prettyPrint(value,level).replaceFirst("domain",name) + case e: ExtendedUserDomainEntry => prettyPrint(value,level).replaceFirst("domain",name) + case _ => s"$name(${prettyPrint(value,level)})" + } + + } + case v: WithSeq => { + v.values.headOption match { + case Some(LitStructEntry(_,_)) => s"[\n$predent${v.values.map(x=>prettyPrint(x,level+1)).mkString(s",\n$predent")}\n$postdent]" + case _ => s"[${v.values.map(x=>prettyPrint(x,level)).mkString(", ")}]" + } + } + case LitPointerEntry(_,v,a, perm) => s"&$a* "/*+ s"(${perm.getOrElse("?")})" */+"-> " ++ prettyPrint(v,level) + case LitAdressedEntry(value, address,perm) => "(" ++prettyPrint(value,level) ++ s") @$address"/* +s" (${perm.getOrElse("?")})" */ + case x => x.toString() + } + } + def removeWhitespace(in: String): String ={ + in.replace(" ","").replace("\t","").replace("\n","") + } + def getSubnodes(s: Vector[PNode]): Seq[PNode] = { + s.flatMap(getSubnodes(_)).toSeq + } + def getSubnodes(o: Option[PNode]): Seq[PNode] = { + o.map(getSubnodes(_)).getOrElse(Seq()) + } + /** + * extracts all subnodes (includeing itself) WARNING do not use on large pnodes (PPackages, large function etc) + * */ + def getSubnodes(a: PNode): Seq[PNode] ={ + val realSubs = a match { + case PPackage(packageClause, programs, _) => getSubnodes(packageClause) ++ programs.flatMap(getSubnodes(_)) + case PProgram(packageClause, imports, _) => getSubnodes(packageClause) ++ imports.flatMap(getSubnodes(_)) + case PPackageClause(id) => getSubnodes(id) + case PExplicitQualifiedImport(qualifier, _) => getSubnodes(qualifier) + case PConstDecl(typ, right, left) => getSubnodes(typ) ++ getSubnodes(right) ++ getSubnodes(left) + case PVarDecl(typ, right, left, _) => getSubnodes(typ) ++ getSubnodes(right) ++ getSubnodes(left) + case PFunctionDecl(id, args, result, spec, body) => getSubnodes(id) ++ getSubnodes(args) ++ getSubnodes(result) ++ getSubnodes(spec) ++getSubnodes(body.map(_._1)) ++getSubnodes(body.map(_._2)) + case PMethodDecl(id, receiver, args, result, spec, body) => getSubnodes(id) ++ getSubnodes(args) ++ getSubnodes(result) ++ getSubnodes(spec) ++getSubnodes(body.map(_._1)) ++getSubnodes(body.map(_._2)) ++getSubnodes(receiver) + case PTypeDef(right, left) => getSubnodes(right) ++ getSubnodes(left) + case PTypeAlias(right, left) => getSubnodes(right) ++ getSubnodes(left) + case PLabeledStmt(label, stmt) => getSubnodes(label) ++ getSubnodes(stmt) + case PExpressionStmt(exp) => getSubnodes(exp) + case PGoStmt(exp) => getSubnodes(exp) + case PDeferStmt(exp) => getSubnodes(exp) + case PExpCompositeVal(exp) => getSubnodes(exp) + case PLength(exp) => getSubnodes(exp) + case PCapacity(exp) => getSubnodes(exp) + case PRange(exp) => getSubnodes(exp) + case PAssert(exp) => getSubnodes(exp) + case PAssume(exp) => getSubnodes(exp) + case PExhale(exp) => getSubnodes(exp) + case PInhale(exp) => getSubnodes(exp) + case PFold(exp) => getSubnodes(exp) + case PUnfold(exp) => getSubnodes(exp) + case PSendStmt(channel, msg) => getSubnodes(channel) ++ getSubnodes(msg) + case PAssignment(right, left) => getSubnodes(right) ++ getSubnodes(left) + case PAssignmentWithOp(right, op, left) => getSubnodes(right) ++ getSubnodes(op) ++ getSubnodes(left) + + case PShortVarDecl(right, left, addressable) => getSubnodes(right)++ getSubnodes(left) + case PIfStmt(ifs, els) => getSubnodes(ifs) ++ getSubnodes(els) + case PIfClause(pre, condition, body) => getSubnodes(pre) ++ getSubnodes(condition) ++ getSubnodes(body) + case PExprSwitchStmt(pre, exp, cases, dflt) => getSubnodes(pre) ++ getSubnodes(exp) ++getSubnodes(cases) ++getSubnodes(dflt) + case PExprSwitchDflt(body) => getSubnodes(body) + case PTypeSwitchDflt(body) => getSubnodes(body) + case PExprSwitchCase(left, body) => getSubnodes(left) ++getSubnodes(body) + case PTypeSwitchStmt(pre, exp, binder, cases, dflt) => getSubnodes(pre) ++ getSubnodes(exp) ++ getSubnodes(binder) ++ getSubnodes(cases) ++getSubnodes(dflt) + + case PTypeSwitchCase(left, body) => getSubnodes(left) ++ getSubnodes(body) + case PForStmt(pre, cond, post, spec, body) => getSubnodes(pre)++getSubnodes(cond)++ getSubnodes(post)++ getSubnodes(spec)++ getSubnodes(body) + case PAssForRange(range, ass, body) => getSubnodes(range) ++ getSubnodes(ass)++ getSubnodes(body) + case PShortForRange(range, shorts, body) => getSubnodes(range) ++getSubnodes(shorts) ++ getSubnodes(body) + + case PSelectStmt(send, rec, aRec, sRec, dflt) => getSubnodes(send)++ getSubnodes(rec)++getSubnodes(aRec)++ getSubnodes(sRec)++ getSubnodes(dflt) + case PSelectDflt(body) => getSubnodes(body) + case PSelectSend(send, body) => getSubnodes(send)++getSubnodes(body) + case PSelectRecv(recv, body) => getSubnodes(recv) ++getSubnodes(body) + case PSelectAssRecv(recv, ass, body) => getSubnodes(recv) ++getSubnodes(ass) ++ getSubnodes(body) + case PSelectShortRecv(recv, shorts, body) => getSubnodes(recv) ++getSubnodes(shorts)++getSubnodes(body) + case PReturn(exps) => getSubnodes(exps) + case PBreak(label) => getSubnodes(label) + case PContinue(label) => getSubnodes(label) + case PGoto(label) => getSubnodes(label) + + case PBlock(stmts) => getSubnodes(stmts) + case PSeq(stmts) => getSubnodes(stmts) + case PNamedOperand(id) => getSubnodes(id) + case PCompositeLit(typ, lit) => getSubnodes(typ) ++ getSubnodes(lit) + case PLiteralValue(elems) => getSubnodes(elems) + case PKeyedElement(key, exp) => getSubnodes(key)++getSubnodes(exp) + case PIdentifierKey(id) => getSubnodes(id) + + case PLitCompositeVal(lit) =>getSubnodes(lit) + case PFunctionLit(args, result, body) => getSubnodes(args) ++ getSubnodes(result) ++ getSubnodes(body) + case PInvoke(base, args) => getSubnodes(base) ++ getSubnodes(args) + case PDot(base, id) => getSubnodes(base) ++getSubnodes(id) + case PIndexedExp(base, index) => getSubnodes(base) ++getSubnodes(index) + + case PSliceExp(base, low, high, cap) => getSubnodes(base) ++getSubnodes(low) ++getSubnodes(high) ++getSubnodes(cap) + case PUnpackSlice(elem) => getSubnodes(elem) + case PTypeAssertion(base, typ) => getSubnodes(base) ++getSubnodes(typ) + case PDeref(base) => getSubnodes(base) + case u: PUnaryExp => getSubnodes(u.operand) + case b: PBinaryExp[PNode,PNode] => getSubnodes(b.left) ++ getSubnodes(b.right) + case PUnfolding(pred, op) => getSubnodes(pred) ++ getSubnodes(op) + case PMake(typ, args) => getSubnodes(typ) ++ getSubnodes(args) + case PNew(typ) => getSubnodes(typ) + case PFPredBase(id) => getSubnodes(id) + case PDottedBase(recvWithId) => getSubnodes(recvWithId) + case PPredConstructor(id, args) =>getSubnodes(id) ++ args.flatMap(getSubnodes(_)) + case PArrayType(len, elem) => getSubnodes(len) ++ getSubnodes(elem) + case PImplicitSizeArrayType(elem) => getSubnodes(elem) + case PSliceType(elem) => getSubnodes(elem) + case PBiChannelType(elem) => getSubnodes(elem) + case PSendChannelType(elem) => getSubnodes(elem) + case PRecvChannelType(elem)=> getSubnodes(elem) + case PVariadicType(elem) => getSubnodes(elem) + case PMapType(key, elem) =>getSubnodes(key)++ getSubnodes(elem) + case PStructType(clauses) => getSubnodes(clauses) + case PFieldDecls(fields) =>getSubnodes(fields) + case PFieldDecl(id, typ) => getSubnodes(id) ++ getSubnodes(typ) + case PEmbeddedDecl(typ, id) => getSubnodes(id) ++ getSubnodes(typ) + case PMethodReceiveName(typ) => getSubnodes(typ) + case PMethodReceivePointer(typ) =>getSubnodes(typ) + case PFunctionType(args, result) => getSubnodes(args) ++ getSubnodes(result) + case PPredType(args) => getSubnodes(args) + case PInterfaceType(embedded, methSpecs, predSpec) => getSubnodes(embedded) ++ getSubnodes(methSpecs) ++ getSubnodes(predSpec) + case PInterfaceName(typ) => getSubnodes(typ) + case PMethodSig(id, args, result, spec, isGhost) => getSubnodes(id) ++getSubnodes(args) ++ getSubnodes(result) ++ getSubnodes(spec) + case PNamedParameter(id, typ) => getSubnodes(id) ++ getSubnodes(typ) + case PUnnamedParameter(typ) => getSubnodes(typ) + case PNamedReceiver(id, typ, addressable) => getSubnodes(typ) ++ getSubnodes(id) + case PUnnamedReceiver(typ) => getSubnodes(typ) + case PResult(outs) =>getSubnodes(outs) + case PEmbeddedName(typ) =>getSubnodes(typ) + case PEmbeddedPointer(typ) =>getSubnodes(typ) + case PFunctionSpec(pres, posts, isPure) => getSubnodes(pres) ++getSubnodes(posts) + case PBodyParameterInfo(shareableParameters) => getSubnodes(shareableParameters) + case PLoopSpec(invariants) => getSubnodes(invariants) + case PExplicitGhostMember(actual) => getSubnodes(actual) + case PFPredicateDecl(id, args, body) => getSubnodes(id) ++ getSubnodes(args) ++ getSubnodes(body) + case PMPredicateDecl(id, receiver, args, body) => getSubnodes(id) ++ getSubnodes(args) ++ getSubnodes(body) ++ getSubnodes(receiver) + case PMPredicateSig(id, args) => getSubnodes(id) ++ getSubnodes(args) + case PImplementationProof(subT, superT, alias, memberProofs) => getSubnodes(subT) ++ getSubnodes(superT) ++ getSubnodes(alias) ++ getSubnodes(memberProofs) + case PMethodImplementationProof(id, receiver, args, result, isPure, body) => getSubnodes(id) ++ getSubnodes(receiver) ++ getSubnodes(args) ++ getSubnodes(result) ++ getSubnodes(body.map(_._1)) ++ getSubnodes(body.map(_._2)) + case PImplementationProofPredicateAlias(left, right) => getSubnodes(left) ++ getSubnodes(right) + case PExplicitGhostStatement(actual) => getSubnodes(actual) + + case POld(operand) => getSubnodes(operand) + case PLabeledOld(label, operand) => getSubnodes(label) ++ getSubnodes(operand) + case PConditional(cond, thn, els) => getSubnodes(cond) ++ getSubnodes(thn) ++ getSubnodes(els) + case PImplication(left, right) => getSubnodes(left) ++ getSubnodes(right) + case PAccess(exp, perm) => getSubnodes(exp) ++ getSubnodes(perm) + case PPredicateAccess(pred, perm) => getSubnodes(pred) ++ getSubnodes(perm) + case PForall(vars, triggers, body) => getSubnodes(vars) ++ getSubnodes(triggers) ++ getSubnodes(body) + case PExists(vars, triggers, body) => getSubnodes(vars) ++ getSubnodes(triggers) ++ getSubnodes(body) + case PTypeOf(exp) => getSubnodes(exp) + case PIsComparable(exp) => getSubnodes(exp) + case POptionNone(t) => getSubnodes(t) + case POptionSome(exp) => getSubnodes(exp) + case POptionGet(exp) => getSubnodes(exp) + case b: PBinaryGhostExp => getSubnodes(b.left)++ getSubnodes(b.right) + case PSequenceConversion(exp) => getSubnodes(exp) + case PGhostCollectionUpdate(col, clauses) => getSubnodes(col) ++ getSubnodes(clauses) + case PGhostCollectionUpdateClause(left, right) => getSubnodes(left) ++ getSubnodes(right) + case PRangeSequence(low, high) => getSubnodes(low) ++ getSubnodes(high) + case PSetConversion(exp) =>getSubnodes(exp) + case PMultisetConversion(exp) =>getSubnodes(exp) + case PMapKeys(exp) =>getSubnodes(exp) + case PMapValues(exp) =>getSubnodes(exp) + case PSequenceType(elem) =>getSubnodes(elem) + case PSetType(elem) =>getSubnodes(elem) + case PMultisetType(elem) =>getSubnodes(elem) + case PMathematicalMapType(keys, values) => getSubnodes(keys) ++ getSubnodes(values) + case POptionType(elem) =>getSubnodes(elem) + case PGhostSliceType(elem) =>getSubnodes(elem) + case PDomainType(funcs, axioms) => getSubnodes(funcs) ++ getSubnodes(axioms) + case PDomainFunction(id, args, result) => getSubnodes(id) ++ getSubnodes(args) ++ getSubnodes(result) + case PDomainAxiom(exp) =>getSubnodes(exp) + case PBoundVariable(id, typ) => getSubnodes(id) ++ getSubnodes(typ) + case PTrigger(exps) => getSubnodes(exps) + case PExplicitGhostParameter(actual) => getSubnodes(actual) + case PExplicitGhostStructClause(actual) => getSubnodes(actual) + case t => Seq() + } + Seq(a) ++ realSubs + } + +} + +class GobraCounterexample(gModel: GobraModelAtLabel) extends Counterexample { + lazy val reducedCounterexample: GobraModel =GobraModel(gModel.labeledEntries.last._2.entries.filterNot(_._2.isInstanceOf[FaultEntry])) + def getRelevantEntries(node: PNode): Seq[((viper.gobra.reporting.Source.Verifier.Info, String), viper.gobra.reporting.GobraModelEntry)] = { + val subnodes= Util.getSubnodes(node) + reducedCounterexample.entries.toSeq.filter(x => subnodes.find(y => x._1._1.pnode.toString.split(" ").head==y.toString).isDefined) + } + def getIrrelevantEntries(node: PNode): Seq[((viper.gobra.reporting.Source.Verifier.Info, String), viper.gobra.reporting.GobraModelEntry)] = { + val subnodes= Util.getSubnodes(node) + reducedCounterexample.entries.toSeq.filterNot(x => subnodes.find(y => x._1._1.pnode.toString.split(" ").head==y.toString).isDefined) + } + + def listOfNodes(node: PNode): Seq[(PNode,GobraModelEntry)] = { + val subnodes = Util.getSubnodes(node) + subnodes.collect(x => reducedCounterexample.entries.toSeq.find( _._1._1.pnode.toString == x)match { case Some(v) => (x,v._2)}) + } + override def toString: String = gModel.toString + + def testString: String = gModel.labeledEntries.head._2.entries.toSeq.sortBy(_._1._1.toString).map(x=>Util.removeWhitespace(s"${x._1._1.toString}\t<- ${Util.prettyPrint(x._2,0).replaceAll("&-?\\d*","&").replaceAll("@-?\\d*","@")}")).mkString(";") + val model = null +} +//for debugging purposes +class GobraNativeCounterexample(s: SiliconMappedCounterexample) extends GobraCounterexample(null) { + override def toString(): String = s.toString +} +class ReducedCounterexample(gModel: GobraModelAtLabel, error: PNode) extends GobraCounterexample(gModel) { + override def toString(): String = getRelevantEntries(error).map(x=>s"${x._1._1.pnode.toString}\t<- ${Util.prettyPrint(x._2,0)}").mkString("\n") +} + +case class GobraModelAtLabel(labeledEntries: Map[String, GobraModel]) { + override def toString: String = { + labeledEntries.map(x=>s"model at label ${x._1}:\n${x._2}").mkString("\n") + } +} +case class GobraModel(entries: Map[(Source.Verifier.Info,String),GobraModelEntry]) { + override def toString: String = { + val params = entries.filter(x=>x._1.isInstanceOf[PParameter]) //first we separate the different types of values + val rest = entries.filterNot(x=>x._1.isInstanceOf[PParameter]) + params.map(x=>s"${x._1._1.pnode.toString}\t<- ${Util.prettyPrint(x._2,0)}").mkString("\n") ++ "\n" ++ + rest.map(x=>s"${x._1._1.pnode.toString}\t<- ${Util.prettyPrint(x._2,0)}").mkString("\n") + + } + +} + +/** this is how we model the values returned by the counterexamples... + * the comments are a different mode of to string that might include more information. + */ + +sealed trait GobraModelEntry{ + override def toString: String = "not implemented" +} + + +sealed trait LitEntry extends GobraModelEntry +sealed trait WithSeq { + val values:Seq[LitEntry] +} + + +case class DummyEntry() extends LitEntry +case class FaultEntry(message: String)extends LitEntry {override def toString = message} +case class LitNilEntry() extends LitEntry { + override def toString(): String = "nil" +} +case class LitIntEntry(value: BigInt) extends LitEntry { + override def toString(): String = s"$value" +} +case class LitBoolEntry(value: Boolean) extends LitEntry { + override def toString(): String = s"$value" +} +case class LitPermEntry(value: viper.silicon.state.terms.Rational) extends LitEntry { + override def toString(): String = s"$value" +} +case class LitOptionEntry(value: Option[LitEntry]) extends LitEntry { + override def toString(): String = s"$value" +} +case class LitSetEntry(values: Set[LitEntry]) extends LitEntry { + override def toString(): String = values.map(_.toString).mkString("{",", ","}") +} +case class LitMSetEntry(values: Map[LitEntry,Int]) extends LitEntry { + override def toString(): String = values.map(x=>s"(${x._1}:${x._2})").mkString("{",", ","}") +} +case class LitArrayEntry(typ: ArrayT, values: Seq[LitEntry]) extends LitEntry with WithSeq { + override def toString(): String = Util.prettyPrint(this, 0)//s"[${values.map(_.toString).mkString(", ")}]" +} +case class LitSliceEntry(typ: SliceT, begin: BigInt, end: BigInt, values: Seq[LitEntry]) extends LitEntry with WithSeq { + override def toString(): String = Util.prettyPrint(this, 0)//s"[${values.map(_.toString).mkString(", ")}]" +} +case class LitSeqEntry(typ: Type, values: Seq[LitEntry]) extends LitEntry with WithSeq { + override def toString(): String = Util.prettyPrint(this, 0)//s"[${values.map(_.toString).mkString(", ")}]" +} +case class LitSparseEntry(full: WithSeq, relevant: Map[(Int, Int), LitEntry]) extends LitEntry { + override def toString():String = relevant.toSeq.sortBy(_._1._1).map(x=>s"${if(x._1._2-x._1._1 <=1)s"${x._1._1}" else s"${x._1._1}-${x._1._2}"}:${x._2}").mkString("[",",","]") +} +case class LitStructEntry(typ:StructT, values: Map[String, LitEntry]) extends LitEntry { + override def toString(): String = /* Util.prettyPrint(this,0) // */s"struct{${values.map(x=>s"${x._1} = ${x._2.toString}").mkString(if(values.size < 5)("; ")else(";\n\t"))}}" + +} +case class UnresolvedInterface(typ: InterfaceT, possibleVals: Seq[GobraModelEntry]) extends LitEntry { + override def toString(): String = "unable to uniquely determine interface. (possibilities include but might not limited to):\n" ++ + ((possibleVals take 3).map(x=>Util.removeWhitespace(x.toString()))).mkString("---\n") ++"\n" +} +case class LitStringEntry(value: String) extends LitEntry { + override def toString(): String = s"${'"'}${value}${'"'}" +} +case class ConcatString(v1: LitEntry, v2: LitEntry) extends LitEntry { + override def toString(): String = s"$v1 + $v2" +} +case class LitPointerEntry(typ: Type, value: LitEntry, address: BigInt,perm: Option[LitPermEntry] = None) extends LitEntry with HeapEntry { + override def toString(): String = s"(&$address*"+ s"(${perm.getOrElse("?")})" + s"-> $value)" +} +//entries that are not designated (typed) as a pointer but are represented by a ref (adressable) +case class LitAdressedEntry(value: LitEntry, address: BigInt, perm: Option[LitPermEntry] = None) extends LitEntry with HeapEntry { + override def toString(): String = s"$value @$address" +s"(${perm.getOrElse("?")})"// not included for easier readability +} +case class LitRecursive(address: BigInt) extends LitEntry { + override def toString(): String = s"&$address (recursive)" +} +case class LitDeclaredEntry(name: String,value: LitEntry) extends LitEntry { + override def toString(): String = { //Util.prettyPrint(this,0) + value match { + case LitStructEntry(_,_) => value.toString().replaceFirst("struct",name) + case LitAdressedEntry(value, address,perm) => LitDeclaredEntry(name,value).toString() ++ s"@$address,(${perm.getOrElse("?")})" + case _: UserDomainEntry | _: ExtendedUserDomainEntry => value.toString.replaceFirst("domain",name) + case _ => s"$name(${value})" + } + } +} + +case class ChannelEntry(typ: ChannelT, buffSize: BigInt, isOpen: Option[Int], isSend: Option[Boolean], isRecieve: Option[Boolean]) extends LitEntry { + override def toString():String = s"(${typ}) [$buffSize] (state: $state" + + s"${if(typ.mod!=ChannelModus.Recv)s", can send: $sending" else ""}" + + s"${if(typ.mod!=ChannelModus.Send)s", can receive: $rec" else ""}" + + ")" + private val state = isOpen match { + case Some(2) => "initialized" + case Some(1) => "created" + case Some(0) => "closed" + case _ => "?" + } + private val sending = isSend match { + case Some(true) => "yes" + case Some(false) => "no" + case _ => "?" + } + private val rec = isRecieve match { + case Some(true) => "yes" + case Some(false) => "no" + case None => "?" + } + + +} +case class FunctionEntry(fname: String, argTypes: Seq[Type], resType: Type, options: Map[Seq[GobraModelEntry], GobraModelEntry], default: GobraModelEntry) extends GobraModelEntry { //maybe extend gobraentry + override def toString: String = { + if (options.nonEmpty) + s"$fname${argTypes.mkString("(",",",")")}:$resType{\n" + options.map(o => " " + o._1.mkString(" ") + " -> " + o._2).mkString("\n") + "\n else -> " + default +"\n}" + else + s"$fname{\n " + default +"\n}" + } +} +//for future use perhaps +case class UserDomain(name: String, typeArgs: Seq[Type], functions: Seq[FunctionEntry]) extends GobraModelEntry {} +case class UserDomainEntry(name: String, id: String) extends LitEntry { + override def toString(): String = name + "_" + id +} + +case class ExtendedUserDomainEntry(original: UserDomainEntry, functions: Seq[FunctionEntry]) extends LitEntry { + override def toString(): String = s"$original${functions.map(f => s"${f.fname} = ${f.options.getOrElse(Seq(original),f.default)}").mkString("{\n\t",if(functions.size > 3)(",\n\t")else(","),"\n}")}" +} + +trait HeapEntry extends GobraModelEntry { + val perm:Option[LitPermEntry] +} +case class LitMapEntry(typ: MapT, value: Map[LitEntry,LitEntry]) extends LitEntry { + override def toString(): String = value.toString() +} + +case class LitPredicateEntry(name: String, args: Seq[LitEntry], perm:Option[LitPermEntry]) extends LitEntry with HeapEntry { + override def toString(): String = s"$name(${args.mkString(",")}) ${perm.getOrElse("?")}" +} +case class UnknownValueButKnownType(info: String, typ: Type) extends LitEntry { + override def toString(): String = s"$info:$typ" +} + +case class FCPredicate(name: String, argsApplied: Option[Seq[LitEntry]], argsUnapplied: Seq[Type]) extends LitEntry { + override def toString(): String = s"$name(${argsApplied.getOrElse(List("?")).mkString("[",",","]")},"++ + s" ${argsUnapplied.mkString((if(argsUnapplied.size==0)"[(fully applied)" else "[_:"),", _:", "]")})" +} + diff --git a/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala b/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala index 65e46dbac..f72ad8720 100644 --- a/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala +++ b/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala @@ -157,14 +157,15 @@ class DefaultErrorBackTranslator( case (l, r) => l orElse r } - override def translate(viperError: viper.silver.verifier.VerificationError): VerificationError = { - val transformedViperError = viperError match { - case err: AbstractVerificationError => err.transformedError() - case err => err + override def translate(viperError: viper.silver.verifier.VerificationError): VerificationError ={ + val ret = DefaultErrorBackTranslator.translateWithTransformer(viperError, errorTransformer) + ret.counterexample = backtrack.config.counterexample match { + case Some(x) => viperError.counterexample match {case Some(x) => CounterexampleBackTranslator(backtrack).translate(x, ret.info.pnode) + case None => None} + case None => None } - DefaultErrorBackTranslator.translateWithTransformer(transformedViperError, errorTransformer) - } - + ret +} override def translate(viperReason: silver.verifier.ErrorReason): VerificationErrorReason = { DefaultErrorBackTranslator.translateWithTransformer(viperReason, reasonTransformer) diff --git a/src/main/scala/viper/gobra/reporting/GobraInterpreter.scala b/src/main/scala/viper/gobra/reporting/GobraInterpreter.scala new file mode 100644 index 000000000..661ca935d --- /dev/null +++ b/src/main/scala/viper/gobra/reporting/GobraInterpreter.scala @@ -0,0 +1,820 @@ +package viper.gobra.reporting +import viper.silicon.{reporting => sil} +import viper.gobra.reporting._ +import viper.gobra.frontend.info.base.Type._ +import viper.gobra.frontend.info.{TypeInfo, ExternalTypeInfo} +import viper.gobra.translator.util.DomainGenerator +import viper.gobra.ast.frontend._ +import viper.gobra.translator.Names +import viper.silver.{ast => vpr} +import scala.util.matching.Regex +import scala.collection.immutable.ListMap + + +trait GobraInterpreter extends sil.ModelInterpreter[GobraModelEntry, Type] +trait GobraDomainInterpreter[T] extends sil.DomainInterpreter[GobraModelEntry, T] + +case class DefaultGobraInterpreter() extends GobraInterpreter{ + override def interpret(entry: sil.ExtractedModelEntry, info: Type): GobraModelEntry = DummyEntry() +} +object InterpreterCache{ + private var heap: Seq[(BigInt, Type)] = Seq() + def isDefined(address: BigInt, typ: Type): Boolean = heap.contains((address, typ)) + def addAddress(address: BigInt, typ: Type): Unit = {heap = (address, typ) +: heap} + def clearCache(): Unit = {heap = Seq(); domains = Seq()} + + private var viperPredicates: Seq[vpr.Predicate] = Seq() + def setPredicates(preds: Seq[vpr.Predicate]): Unit = {viperPredicates = preds} + def clearPreds(): Unit = {viperPredicates = Seq()} + def getPreds(): Seq[vpr.Predicate] = viperPredicates + + private var gobraPredicates: Seq[PFPredicateDecl] = Seq() + def setGobraPredicates(preds:Seq[PFPredicateDecl]): Unit = {gobraPredicates = preds} + def clearGobraPreds(): Unit = {gobraPredicates = Seq()} + def getGobraPreds(): Seq[PFPredicateDecl] = gobraPredicates + + private var typeInfo : viper.gobra.frontend.info.ExternalTypeInfo = null + def setTypeInfo(info: viper.gobra.frontend.info.ExternalTypeInfo): Unit = {typeInfo = info} + def getType(pnode: PNode): Type = { + pnode match { + case (x: PIdnNode) => typeInfo.typ(x) + case (x: PParameter) => typeInfo.typ(x) + case (x: PExpression) => typeInfo.typ(x) + case (x: PMisc) => typeInfo.typ(x) + case _ => UnknownType + } + } + private var domains: Seq[UserDomainEntry] = Seq() + def existsDomain(d: UserDomainEntry): Boolean = domains.contains(d) + def addDomain(d: UserDomainEntry): Unit = {domains = d +: domains} + +} + +/** + * interprets all Extracted values to Gobra values using its sub interpreters for each individual type + * + * @param c + */ +case class MasterInterpreter(c: sil.Converter) extends GobraInterpreter{ + val optionInterpreter: GobraDomainInterpreter[OptionT] = OptionInterpreter(c) + val productInterpreter: GobraDomainInterpreter[StructT] = ProductInterpreter(c) + val sharedStructInterpreter : GobraDomainInterpreter[StructT] = SharedStructInterpreter(c) + val boxInterpreter: GobraDomainInterpreter[Type] = BoxInterpreter(c) + val indexedInterpreter: GobraDomainInterpreter[ArrayT] = IndexedInterpreter(c) + val sliceInterpreter: GobraDomainInterpreter[SliceT] = SliceInterpreter(c) + val pointerInterpreter : sil.AbstractInterpreter[sil.RefEntry, Type, GobraModelEntry] = PointerInterpreter(c) + val interfaceInterpreter: GobraDomainInterpreter[InterfaceT] = InterfaceInterpreter(c) + val channelInterpreter: sil.AbstractInterpreter[sil.LitIntEntry, ChannelT, GobraModelEntry] = ChannelInterpreter(c) + def interpret(entry: sil.ExtractedModelEntry, info: Type): GobraModelEntry = { + entry match{ + case sil.LitIntEntry(v) => info match { + case StringT => StringInterpreter(c).interpret(entry, null) + case DeclaredT(d, c) => val name = d.left.name + val actual = interpret(entry, c.symbType(d.right)) match { + case l: LitEntry => l + case _ => FaultEntry("not a lit entry") + } + LitDeclaredEntry(name, actual) + case ch: ChannelT => channelInterpreter.interpret(sil.LitIntEntry(v), ch) + case _ => LitIntEntry(v) + } + case sil.LitBoolEntry(b) => info match{ + case DeclaredT(d, c) => val name = d.left.name; LitDeclaredEntry(name, LitBoolEntry(b)) + case _ => LitBoolEntry(b) + } + case sil.LitPermEntry(p) => LitPermEntry(p) + case _: sil.NullRefEntry => LitNilEntry() + case v: sil.VarEntry => interpret(c.extractVal(v), info) + case d: sil.DomainValueEntry => if(d.getDomainName.contains("Embfn$$")){ + boxInterpreter.interpret(d, info) + }else{ + info match { + case t: OptionT => optionInterpreter.interpret(d, t) + case t: StructT => if(d.getDomainName.startsWith("ShStruct")) + sharedStructInterpreter.interpret(d, t) + else + productInterpreter.interpret(d, t) + case t: ArrayT => if(d.getDomainName.startsWith("Slice")){ + sliceInterpreter.interpret(d, SliceT(t.elem)) + }else{ + indexedInterpreter.interpret(d, t) + } + + case t: SliceT => sliceInterpreter.interpret(d, t) + case DeclaredT(decl, cont) => cont.symbType(decl.right) match { + case _: DomainT => UserDomainInterpreter(c).interpret(d, DeclaredT(decl, cont)) + case t => val name = decl.left.name + val actual = interpret(entry, t) match { + case l: LitEntry => l + case _ => FaultEntry("not a lit entry") + } + LitDeclaredEntry(name, actual) + } + + case i: InterfaceT => interfaceInterpreter.interpret(d, i) + case p: PointerT => val newType = p.elem match { + case a: ArrayT => sharedTypify(a) + case x => x + } + val adress = PointerInterpreter(c).nameToInt("*!1000", p.elem.toString) + interpret(entry, p.elem) match { + case LitAdressedEntry(value, address, perm) => LitPointerEntry(p.elem, value, address, perm) + case p: LitPointerEntry => p + case LitDeclaredEntry(name, LitAdressedEntry(value, address, perm)) => LitPointerEntry(p.elem, LitDeclaredEntry(name, value), address, perm) + case LitDeclaredEntry(_, LitNilEntry()) => LitNilEntry() + case x: LitEntry => LitPointerEntry(p.elem, x, adress) + } + case pred: PredT => PredicateInterpreter(c).interpret(d, pred) + case dom: DomainT => UserDomainInterpreter(c).interpret(d, DeclaredT(PTypeDef(dom.decl, PIdnDef("domain")), dom.context)) + case GhostSliceT(elem) => sliceInterpreter.interpret(d, SliceT(elem)) + case x => FaultEntry(s"$x ${DummyEntry()}") + }} + case sil.ExtendedDomainValueEntry(o, i) => interpret(o, info) + case r: sil.RefEntry => pointerInterpreter.interpret(r, info) + case rr: sil.RecursiveRefEntry => info match{ + case t: PointerT => {val address = PointerInterpreter(c).nameToInt(rr.name, PointerInterpreter(c).filedname(rr, t.elem)) + LitAdressedEntry(FaultEntry(s"recursive call"), address) + } + case _ => FaultEntry("recursive reference to non pointer... how?") + } + case s: sil.SeqEntry => + info match { + case a: ArrayT=> val (values, map) = interpretSeq(s.values, a.elem) + if(values.size <= 10) LitArrayEntry(a, values) else LitSparseEntry(LitArrayEntry(a, values), map) + case a: SequenceT => val (values, map) = interpretSeq(s.values, a.elem) + if(values.size <= 10) LitSeqEntry(a, values) else LitSparseEntry(LitSeqEntry(a, values), map) + case a: GhostSliceT => val (values, map) = interpretSeq(s.values, a.elem) + if(values.size <= 10) LitSeqEntry(a, values) else LitSparseEntry(LitSeqEntry(a, values), map) + case _ => FaultEntry(s"${info.getClass()} not implemented") + } + case sil.PredHeapEntry(name, args, perm) => info match { + case PredT(types) => LitPredicateEntry(name, + args.zip(types).map(x => interpret(x._1, x._2).asInstanceOf[LitEntry]), + perm.map(LitPermEntry)) + case _ => FaultEntry(s"Predicate type expected but found: $info") + } + case _ => FaultEntry(s"illegal call of interpret: ${entry}") + } + } + def interpretSeq(vals: Seq[sil.ExtractedModelEntry], typ: Type): (Seq[LitEntry], Map[(Int, Int), LitEntry]) = {//used for sparsity (might affect performance) + var first = 0; + var second = (-1); + var curr: LitEntry = null; + var map: Map[(Int, Int), LitEntry] = Map() + val ret = vals.map(x => interpret(x, typ) match { + case l: LitEntry => + second = second + 1 + if(l != curr){ + map = map ++ Map((first, second) -> curr) + curr = l + first = second + };l + case _ => FaultEntry("Could not resolve Element") + }) + map = (map-((0, 0)))++ Map((first, second + 1) -> curr) + (ret, map) + } + //deprecated type of a shared type + def sharedTypify(old: Type):Type = { + old match { + case DeclaredT(d, c) => val actual = sharedTypify(c.symbType(d.right)) + actual + case ArrayT(l, elem) => ArrayT(l, PointerT(elem)) + case StructT(clauses, decl, context) => StructT(clauses.map(x => (x._1, (x._2._1, PointerT(x._2._2)))), decl, context) + case x => x + } + } + +} + +case class OptionInterpreter(c: sil.Converter) extends GobraDomainInterpreter[OptionT]{ + val nonFuncName: String = Names.optionIsNone + val getFuncName: String = Names.optionGet + def interpret(entry: sil.DomainValueEntry, info: OptionT): GobraModelEntry = { + val doms = c.domains.filter(x => x.valueName == entry.domain) + if(doms.length == 1){ + val functions: Seq[sil.ExtractedFunction] = doms.head.functions + val noneFunc: sil.ExtractedFunction = functions.find(_.fname == nonFuncName) match { + case Some(value) => value; + case None => return FaultEntry(s"${entry}: could not relsove, ($nonFuncName) not found")} + val getFunc: sil.ExtractedFunction = functions.find(_.fname == getFuncName) match { + case Some(value) => value; + case None => return FaultEntry(s"${entry}: could not relsove, ($getFuncName) not found") + } + val isNone: Boolean = noneFunc.apply(Seq(entry)) match { + case Right(sil.LitBoolEntry(b)) => b + case _ => return FaultEntry(s"${entry}: could not relsove ($nonFuncName)") + } + if(isNone){ + LitOptionEntry(None) + }else{ + val actualval: sil.ExtractedModelEntry = getFunc.apply(Seq(entry)) match { + case Right(v) => v + case _ => return FaultEntry(s"${entry}: could not relsove ($getFuncName)") + } + val gobraval = MasterInterpreter(c).interpret(actualval, info.elem) match { + case e: LitEntry => e + case x => return FaultEntry(s"internal error: ${x}") + } + LitOptionEntry(Some(gobraval)) + } + }else{ + FaultEntry(s"could not relsove domain: ${entry.domain}") + } + } +} +case class ProductInterpreter(c: sil.Converter) extends GobraDomainInterpreter[StructT]{ + def getterFunc(i: Int, n: Int) = Names.getterFunc(i, n) + def interpret(entry: sil.DomainValueEntry, info: StructT): GobraModelEntry = { + val doms = c.domains.find(_.valueName == entry.domain) + if(doms.isDefined){ + val functions: Seq[sil.ExtractedFunction] = doms.get.functions + val fields = info.fields + val numFields = fields.size + val getterNames = Seq.range(0, numFields).map(getterFunc(_, numFields)) + val getterfuncs = getterNames.map(x => functions.find(n => (n.fname == x || n.fname == s"ShStruct$x"))).collect({case Some(v) => v}) + val fieldToVals = (fields.keys.toSeq.zip(getterfuncs).map( + x => (x._1, x._2.apply(Seq(entry)) match {case Right(v) => v; + case _ => return FaultEntry(s"${entry}: could not relsove (${x._1})") + }) + )).toMap + try{ + val values = fields.map(x => (x._1, MasterInterpreter(c).interpret(fieldToVals.apply(x._1), x._2) match{ + case l: LitEntry => l; + case _ => return FaultEntry("internal error struct") + } + )) + LitStructEntry(info, values) + }catch{ + case t: Throwable => return FaultEntry(s"${entry.domain} wrong domain for type: ${info.toString.replace("\n", ";")}") + } + + }else{ + FaultEntry(s"could not relsove domain: ${entry.domain}") + } + } +} +case class SharedStructInterpreter(c: sil.Converter) extends GobraDomainInterpreter[StructT] { +def getterFunc(i: Int, n: Int) = Names.sharedStructDomain ++ Names.getterFunc(i, n) + def interpret(entry: sil.DomainValueEntry, info: StructT): GobraModelEntry = { + val doms = c.domains.find(_.valueName == entry.domain) + if(doms.isDefined){ + val functions: Seq[sil.ExtractedFunction] = doms.get.functions + val fields = info.fields + val numFields = fields.size + val getterNames = Seq.range(0, numFields).map(getterFunc(_, numFields)) + val getterfuncs = getterNames.map(x => functions.find(n => n.fname == x)).collect({case Some(v) => v}) + val fieldToVals = (fields.keys.toSeq.zip(getterfuncs).map( + x => (x._1, x._2.apply(Seq(entry)) match {case Right(v) => v; + case _ => return FaultEntry(s"${entry}: could not relsove (${x._1})") + }) + )).toMap + val mem = Integer.parseInt(entry.id) + val offset = (entry.domain).hashCode.abs % 100 + var address = BigInt( mem * 100 + (if(mem != 0) offset else 0) ) // shuld be 0 if we are dealing with the default value + try{ + + val values = fields.map(x => (x._1, MasterInterpreter(c).interpret(fieldToVals.apply(x._1), PointerT(x._2)) match{ + case p: LitPointerEntry => if(address == 0){address = offset}; LitAdressedEntry(p.value, p.address, p.perm) + case l: LitEntry => l; + case _ => return FaultEntry("internal error struct") + } + )) + LitAdressedEntry(LitStructEntry(info, values), address) + }catch{ + case t: Throwable =>/* printf(s"$t"); */return FaultEntry(s"${entry.domain} wrong domain for type: ${info.toString.replace("\n",";")}") + } + + }else{ + FaultEntry(s"could not relsove domain: ${entry.domain}") + } + } +} +//used for embedding +case class BoxInterpreter(c: sil.Converter) extends GobraDomainInterpreter[Type] { + def unboxFunc(domain: String) = s"${Names.embeddingUnboxFunc}_$domain" + def boxFunc(domain: String) = s"${Names.embeddingBoxFunc}_$domain" + def interpret(entry: sil.DomainValueEntry, info: Type): GobraModelEntry = { + val functions = c.non_domain_functions + val unbox = functions.find(_.fname == unboxFunc(entry.domain)) + val box = functions.find(_.fname == boxFunc(entry.domain)) + if(unbox.isDefined && box.isDefined){ + val unboxed: sil.ExtractedModelEntry = try{Right(unbox.get.options.head._2) match{ //unboxing has some strange behaviour. + case Right(x) => x + case _ => return FaultEntry(s"wrong application of function $unbox") + } + }catch { + case _: Throwable => unbox.get.default + } + MasterInterpreter(c).interpret(unboxed, info) + }else{ + FaultEntry(s"${unboxFunc(entry.domain)} not found") + } + } +} +case class IndexedInterpreter(c: sil.Converter) extends GobraDomainInterpreter[ArrayT] { + def lenName(d: String) = Names.length(d) + def index(d: String) = Names.location(d) + def interpret(entry: sil.DomainValueEntry, info: ArrayT): GobraModelEntry = { + val doms = c.domains.find(_.valueName == entry.domain) + if(doms.isDefined){ + val functions: Seq[sil.ExtractedFunction] = doms.get.functions + val lengthFunc = functions.find(_.fname == lenName(doms.get.name)) + val length = lengthFunc match{ + case Some(value) => value.apply(Seq(entry)) match{ + case Right(i: sil.LitIntEntry) => i.value + case _ => return FaultEntry("length ill defined") + } + case None => return FaultEntry("length not found") + } + val offsetFunc = functions.find(_.fname == index(doms.get.name)) + var address: BigInt = 0; + var first = 0; + var second = (-1); + var curr: LitEntry = null; + var map: Map[(Int, Int), LitEntry] = Map() + if(offsetFunc.isDefined){ + val indexFunc = offsetFunc.get + val values = 0.until(length.toInt).map(i => { + val x = indexFunc.apply(Seq(entry, sil.LitIntEntry(i))) match{ + case Right(x) => MasterInterpreter(c).interpret(x, info.elem) match { + case a: LitAdressedEntry => address += a.address; a.value + case x: LitEntry => x + case _ => FaultEntry("not a literal") + } + case _ => return FaultEntry("could not resolve") + } + //for sparsity + second = second + 1 + if(x != curr){ + map = map ++ Map((first, second) -> curr) + curr = x + first = second + } + x + }) + + map = Map((first, second + 1) -> curr) ++ (map - ((0, 0))) + val value = if(length <= 10 || map.size-values.size < 5) LitArrayEntry(info, values) else LitSparseEntry(LitArrayEntry(info, values), map) + if(address == 0){ + value + }else{ + LitAdressedEntry(value, address) + } + + }else{ + FaultEntry(s"offset not found") + } + + }else{ + FaultEntry(s"could not relsove domain: ${entry.domain}") + } + } +} +case class SliceInterpreter(c: sil.Converter) extends GobraDomainInterpreter[SliceT]{ + val sarray = Names.sliceArray + val soffset = Names.sliceOffset + val slen = Names.sliceLength + def interpret(entry: sil.DomainValueEntry, info: SliceT): GobraModelEntry = { + val doms = c.domains.find(_.valueName == entry.domain) + if(doms.isDefined){ + val functions = doms.get.functions + val funcSarray = functions.find(_.fname == sarray) + val funcOffset = functions.find(_.fname == soffset) + val funclength = functions.find(_.fname == slen) + if(funclength.isDefined && funcOffset.isDefined && funcSarray.isDefined){ + val length = funclength.get.apply(Seq(entry)) match{ + case Right(i: sil.LitIntEntry) => i.value + case _ => return FaultEntry("length not defined") + } + val offset = funcOffset.get.apply(Seq(entry)) match{ + case Right(i: sil.LitIntEntry) => i.value + case _ => return FaultEntry("offset not defined") + } + + val (array, arraytyp, locfun: sil.ExtractedFunction) = funcSarray.get.apply(Seq(entry)) match { + case Right(x) => x match { + case v: sil.VarEntry => c.extractVal(v) match { + case s: sil.SeqEntry => (s, ArrayT(s.values.size, info.elem), null) + case _ => return FaultEntry("extracted Value not a sequence") + } + case s: sil.SeqEntry => (s, ArrayT(s.values.size, info.elem), null) // same here + case d: sil.DomainValueEntry => (d, ArrayT(0, PointerT(info.elem)), + c.domains.find(_.valueName == d.domain).get.functions.find(_.fname == Names.location(d.getDomainName)).get.apply(Seq(d)) match{ + case Left(f) => f + case _ => return FaultEntry("function ShArrayloc not found...") + } + ) + case _ => (sil.OtherEntry("internal","error"), UnknownType, null) + } + case _ => return FaultEntry(s"$sarray false application") + } + /* deprecated, getting the entire arry instead of only the relevant idices + val original = MasterInterpreter(c).interpret(array, arraytyp) match { + case x:LitArrayEntry => x + case _=> return FaultEntry("not an array") + } */ + + var first = 0; //TODO: possibly move this to MasterInterpreter.interpretSeqs + var second = (-1); + var curr: LitEntry = null; + var map: Map[(Int, Int), LitEntry] = Map() + // directly get the values from the indices + def loc(v: BigInt) = { + + val x = locfun.apply(Seq(sil.LitIntEntry(v))) match { + case Right(t) => MasterInterpreter(c).interpret(t, PointerT(info.elem)) match { + case p: LitPointerEntry => InterpreterCache.clearCache();p.value + case a: LitAdressedEntry => InterpreterCache.clearCache();a.value + case n: LitNilEntry => if(info.elem.isInstanceOf[PointerT]) n else Util.getDefault(info.elem).asInstanceOf[LitEntry] + case l: LitEntry => l + } + case _ => FaultEntry("not resolvable function loc") + } + //again sparsity + second = second + 1 + if(x != curr){ + map = map ++ Map((first, second) -> curr) + curr = x + first = second + } + x + } + val values = (offset until (offset + length)).map(x => loc(x)) + val value = LitSliceEntry(info, offset, offset + length, values) + //hedge problem fix + map = Map((first, second + 1) -> curr) ++ (map - ((0, 0))) + if(values.size <= 10) value else LitSparseEntry(value, map) + }else{ + FaultEntry(s"functions ($sarray, $soffset, $slen) not found") + } + + }else{ + FaultEntry(s"${entry.domain} not found") + } + } +} + +case class PointerInterpreter(c: sil.Converter) extends sil.AbstractInterpreter[sil.RefEntry, Type, GobraModelEntry]{ + + def interpret(entry: sil.RefEntry, info: Type): GobraModelEntry = { + + info match{ + case PointerT(elem ) => { + val field = filedname(entry, elem) + val address = nameToInt(entry.name, field) + if(InterpreterCache.isDefined(address, info)){ + return LitRecursive(address) + } + val extracted: sil.RefEntry = c.extractVal(sil.VarEntry(entry.name, viper.silicon.state.terms.sorts.Ref)) match{ + case r: sil.RefEntry => r + case _ => return FaultEntry("false extraction") + } + // + val eField = extracted.fields.getOrElse(field, (sil.OtherEntry(s"$field: Field not found", s"help"), None)) + val perm = eField._2.map(LitPermEntry(_)) + val fieldval = if(extracted.fields.isEmpty) return LitNilEntry() + else if(eField._1.isInstanceOf[sil.OtherEntry]) extracted.fields.head._2._1 match { + case r: sil.RefEntry => val value = interpret(r, info); return LitAdressedEntry(value.asInstanceOf[LitEntry], nameToInt(entry.name, filedname(entry, info)), perm) + case n: sil.NullRefEntry => return LitNilEntry() + case x => x + } + InterpreterCache.addAddress(address, info); + val value = eField._1 match { + case x: sil.OtherEntry => FaultEntry(s"not Found Field:$field but found $fieldval in ${extracted.fields.head._1}") + case r: sil.RefEntry => interpret(r, elem) match { + case LitAdressedEntry(value, a, p) => return LitAdressedEntry(LitPointerEntry(elem, value.asInstanceOf[LitEntry], a, p), address, perm) + case x => x + } + case t => MasterInterpreter(c).interpret(t, elem) + } + LitPointerEntry(elem, value.asInstanceOf[LitEntry], address, perm) + } + case t => { + // we are actually handling an shared value + val address = nameToInt(entry.name, filedname(entry, t)) + val value = interpret(entry, PointerT(t)) + value match { + case p: LitPointerEntry => LitAdressedEntry(p.value, address, p.perm) + case n: LitNilEntry => Util.getDefault(t) + case x: LitEntry => LitAdressedEntry(x, address) + } + } + } + + } + //used for address encoding + def nameToInt(name: String, field: String): Int = { + try{ + val id = Integer.parseInt(name.split("!").last) + val offset = field.hashCode() + (id + 1) * 100 + (offset % 100) + }catch{ + case _: NumberFormatException => 0 + } + } + + def filedname(entry: sil.ExtractedModelEntry, i: Type): String = { //TODO: improve (maybe move to encoding of them) + i match { + case _: IntT => Names.pointerField(vpr.Int) + case BooleanT => Names.pointerField(vpr.Bool) + case StringT => Names.pointerField(vpr.Int) + case PointerT(elem) => elem match{ + case x: StructT => Names.pointerField(vpr.Int).replace("Tuple","ShStruct") + case d: DeclaredT => filedname(entry, d.context.symbType(d.decl.right)) + case _ => Names.pointerField(vpr.Ref) + } + case d: DeclaredT => filedname(entry, d.context.symbType(d.decl.right)) + case x: StructT => entry match { + case r: sil.RefEntry => s"val$$_ShStruct${x.fields.size}${if(x.fields.size == 0)""else "_"}${"Ref".repeat(x.fields.size)}" + case _ => s"val$$_Tuple${x.fields.size}_${x.fields.map(x => filedname(null, x._2).replaceFirst("val$$_Tuple", ""))}" + } + case InterfaceT(decl, context) => "val$_Tuple2_RefTypes" + case DomainT(decl, context) => "TODO: domains" + case ch: ChannelT => Names.pointerField(vpr.Int) + case s: SliceT => "val$_Slice_Ref" + case x => s"$x" + } + } +} + + + +case class StringInterpreter(c: sil.Converter) extends sil.ModelInterpreter[GobraModelEntry, Any] { + val stringDomain = Names.stringsDomain + val prefix = Names.stringPrefix + def interpret(entry: sil.ExtractedModelEntry, info: Any): GobraModelEntry = { + val doms = c.domains.find(_.valueName == stringDomain) + if(doms.isDefined){ + val functions: Seq[sil.ExtractedFunction] = doms.get.functions + entry match{ + case e: sil.LitIntEntry => functions.find(x => x.fname.startsWith(prefix) && x.default == e) match {//regular string lit case + case Some(f) => { val hex: String = f.fname.stripPrefix(prefix) + val value = hexToChar(toArray(hex)) + LitStringEntry(value) + + } + case _=> functions.find(x => x.fname == Names.stringConact && x.image.contains(e)) match {//concatination case + case Some(f) => {val origs = f.options.find(_._2 == e).getOrElse(return FaultEntry("Concatitnation of undeterminable values")) + val (first, second) = (origs._1.head, origs._1.last) + val ret = (interpret(first, null), interpret(second, null)) match { + case (x: LitStringEntry, y: LitStringEntry) => LitStringEntry(x.value + y.value) + + case (x, y) => ConcatString(x.asInstanceOf[LitEntry], y.asInstanceOf[LitEntry]) + } + ret + } + case _ => FaultEntry("string literal not found") //probably empty string but no guarantee... + } + } + + case _=> FaultEntry("could not resolve string because not an Int Entry") + } + }else{ + FaultEntry("could not resolve string") + } + } + def hexToChar(input: Seq[Byte]): String = { + input.map(_.toChar).mkString + } + def toArray(input: String): Seq[Byte] = { + org.apache.commons.codec.binary.Hex.decodeHex(input.toCharArray()) + } +} +case class InterfaceInterpreter(c: sil.Converter) extends GobraDomainInterpreter[InterfaceT]{ + def interpret(entry: sil.DomainValueEntry, info: InterfaceT): GobraModelEntry = { + val doms = c.domains.find(_.valueName == entry.domain) + if(doms.isDefined){ + val valuefunc = doms.get.functions.find(_.fname == Names.getterFunc(0, 2))match{case Some(x) => x ; case _ => return FaultEntry("Value function not defined")} + val typfunc = doms.get.functions.find(_.fname == Names.getterFunc(1, 2))match{case Some(x) => x ; case _ => return FaultEntry("no type function?")} + val value = valuefunc.apply(Seq(entry)) match{case Right(v) => v} + val typ = typfunc.apply(Seq(entry)) match{case Right(v) => v} + val typeDom = c.domains.find(_.valueName == Names.typesDomain).get + //either which it is or a list ow which it could be + val typeinfo = getType(typ, typeDom) + val typeDecls = info.context.asInstanceOf[TypeInfo].tree.nodes.collect({case x: PTypeDecl => x}) + val gobraType = typeinfo match { + case (Left(v), p) => { + // we can find out which named type it is TODO: make named finding better (e.g named with _ in them) + + val declaredT = fnameToType(v.fname, info.context) match { + case Right(x) => x + case Left(x) => return x + } + if(p){ + PointerT(declaredT) + }else{ + declaredT + } + } + case (Right(o), p) => { + val opts = get_options(o, value, typeDecls, info.context) + if(opts.length > 1) return UnresolvedInterface(info, opts) + else if(opts.length == 1) return opts.head // there is only one option this must be the one + else if(p) return FaultEntry("possibly nil") + else return FaultEntry("possibly empty interface") + } + } + val fieldName = PointerInterpreter(c).filedname(if(typeinfo._2){sil.RefEntry("l", null)} else {sil.LitBoolEntry(false)}, gobraType) + //ISSUE: we do not know the (viper) type of the entry... + val polyDom = c.domains.find(x => isSamePoly(x.valueName, fieldName)) + val viperVal = polyDom match{ + case Some(x) => { + x.functions.find(_.fname == "unbox_Poly").get.apply(Seq(value)) match { case Right(x) => x} + } + case _ => try{ + c.extractVal(value.asInstanceOf[sil.VarEntry]) + }catch{case _: Throwable => return FaultEntry(s"no corresponding Polymorphism for ${fieldName.drop(5).takeWhile(_ != '_')}")} + } + MasterInterpreter(c).interpret(viperVal, gobraType) + }else{ + FaultEntry(s"${entry.domain} not found") + } + + } + + def isSamePoly(domName: String, typeName: String): Boolean = { + val ts = domName.drop(5).replace('[', '_') + .replace("]", "") + .replace(",", "") // a parameterized Viper type uses comma-space separated types if there are multiple + .replace(" ", "") + s"val$$_$ts" == typeName + } + //extract type from the constructor function + def fnameToType(fname: String, context: ExternalTypeInfo): Either[GobraModelEntry, Type] = { + val typeDecls = context.asInstanceOf[TypeInfo].tree.nodes.collect({case x: PTypeDecl => x }) + val namedName = fname.takeWhile(_ != '_') + typeDecls.find(_.left.name == namedName) match { + case Some(decl) => Right(DeclaredT(decl, context)) + case _ => namedName match { + case "nil" => Left(FaultEntry("probably nil interface")) + case "empty" => Left(FaultEntry("probably empty interface")) + case "struct" => context.asInstanceOf[TypeInfo].tree.nodes.collect({case x: PStructType => x}) match { + case Nil => Left(FaultEntry("no struct decalaration in scope")) + case s => Right(StructT(ListMap() ++ (s.head.fields.map(x => ((x.id.toString, (true, Util.getType(x.typ, context)))))).toMap[String, (Boolean, viper.gobra.frontend.info.base.Type.Type)], s.head, context)) //TODO find the types of the clauses + + } + case _ => Left(FaultEntry(s"could not resolve $namedName")) + } + + } + } + + // get the correct function from the pointers + def getType(typ: sil.ExtractedModelEntry, typeDom: sil.DomainEntry): (Either[sil.ExtractedFunction, Seq[sil.ExtractedFunction]], Boolean) = { + //TODO: handle pointer to pointer + val pointerfunc = typeDom.functions.find(_.fname == "pointer_Types") + val isreversable = pointerfunc.isDefined && pointerfunc.get.options.values.toSeq.contains(typ) + val isDefault= pointerfunc.isDefined && pointerfunc.get.default == typ + if(isreversable){ + val actualtyp = pointerfunc.get.options.toSeq.find(_._2 == typ).get._1.head + val corr_typ_func = typeDom.functions.find(_.default == actualtyp) match{case Some(x) => x} + (Left(corr_typ_func), true) + + }else if(isDefault){ + val isNot = pointerfunc.get.options.map(_._1) + val corr_types = typeDom.functions.filterNot(y => (isNot.find(_ == y.default).isDefined || isnonTypeFunction(y.fname))) + (Right(corr_types.toSeq), true) + } + else{ + val corr_typ_func = typeDom.functions.find(_.default == typ) match{case Some(x) => x ; + case _ => typeDom.functions.find(_.fname == s"${Names.emptyInterface}_Types") match { + case Some(x) => x + case _ => typeDom.functions.find(_.fname == "nil_Types") match{ + case Some(x) => x + case _=> return (Right(Seq()), false) + } + } + } + (Left(corr_typ_func), false) + } + } + //get all posibilities of values the + def get_options(functions: Seq[sil.ExtractedFunction], value: sil.ExtractedModelEntry, typedecls: Seq[PTypeDecl], context: ExternalTypeInfo): Seq[GobraModelEntry] = { + val names = functions.map(_.fname.takeWhile(_ != '_')) + val declarations = typedecls.collect(x => {if(names.contains(x.left.name.toString)) Some(DeclaredT(x, context))else None} ).collect(_ match {case Some(x) => x}) + val fieldNameswithtyps = declarations map (x => (PointerInterpreter(c).filedname(sil.RefEntry("l", null), PointerT(x)), PointerT(x))) + + val polysandtyps = fieldNameswithtyps.collect(f => c.domains.find(d => isSamePoly(d.valueName, f._1))match{case Some(x) => (x, f._2)}) + val relevantpolys = polysandtyps.filter(x => isPointerViper(x._1.valueName.drop(5))) + //TODO: more filtering? + val withcorrectunbox = relevantpolys.filter(x => x._1.functions.find(_.fname == "box_Poly")match {case Some(f) => f.image.contains(value) }) + val values = relevantpolys.collect(x => x._1.functions.find(_.fname == "unbox_Poly") match {case Some(f) => f.apply(Seq(value)) match{case Right(r) => (r, x._2)} } ) + values.map(x => MasterInterpreter(c).interpret(x._1, x._2)) + } + def isPointerViper(name: String): Boolean = { + name.startsWith("Sh") || name.equals("Ref") + } + //filter out functions that are irrelevant + def isnonTypeFunction(fname: String): Boolean = {//TODO: make this smarter + fname.startsWith(Names.emptyInterface) || + fname.startsWith(Names.toInterfaceFunc) || + fname.startsWith(Names.typeOfFunc) || + fname.startsWith(Names.dynamicPredicate) || + fname.startsWith(Names.implicitThis) + } +} +case class ChannelInterpreter(c: sil.Converter) extends sil.AbstractInterpreter[sil.LitIntEntry, ChannelT, GobraModelEntry] { + def interpret(entry: sil.LitIntEntry, info: ChannelT): GobraModelEntry = { + val preds = c.extractedHeap.entries.filter(x => x.isInstanceOf[sil.PredHeapEntry]&&x.asInstanceOf[sil.PredHeapEntry].args == Seq(entry)) + if(entry.value == 0){ + return LitNilEntry() + } + //TODO: move to Names + val isSend = preds.find(_.toString.startsWith("SendChannel")) match {case Some(x) => interPerm(x.asInstanceOf[sil.PredHeapEntry]);case None => Some(false)} + val isRecv = preds.find(_.toString.startsWith("RecvChannel")) match {case Some(x) => interPerm(x.asInstanceOf[sil.PredHeapEntry]);case None => Some(false)} + val isOpen = preds.find(_.toString.startsWith("IsChannel")) match { + case Some(x) => if (interPerm(x.asInstanceOf[sil.PredHeapEntry]).getOrElse(false)) {if(isRecv.getOrElse(false)||isSend.getOrElse(false)) Some(2) else Some(1)} else Some(0) + case None => if(isRecv.getOrElse(false)||isSend.getOrElse(false)) Some(2) else None } + val buffSize = c.non_domain_functions.find(_.fname.startsWith("BufferSize")) match { + case Some(x) => x.apply(Seq(entry)) match { + case Right(sil.LitIntEntry(v)) => v; + case _=> BigInt(0)} + case _ => return FaultEntry("buffsize not found") + } + ChannelEntry(info, buffSize, isOpen, isSend, isRecv) + } + def interPerm(x: sil.PredHeapEntry): Option[Boolean] = { + import viper.silicon.state.terms._ + x.perm match{ + case Some(Rational.zero) => Some(false) + case Some(Rational.one) => Some(true) + case Some(x) if(x > Rational(0, 1)) => Some(true) + case _ => None + } + } +} +/** + * experimental Predicate interpreter + */ +case class PredicateInterpreter(c: sil.Converter) extends GobraDomainInterpreter[PredT] { + def interpret(entry: sil.DomainValueEntry, info: PredT) = { + val preds = c.extractedHeap.entries.filter(x => x.isInstanceOf[sil.PredHeapEntry]) + val domOpt = c.domains.find(_.valueName == entry.domain) + val symbolConv = new viper.silicon.state.DefaultSymbolConverter + if( domOpt.isDefined){ + val dom = domOpt.get + val corr_function = dom.functions.find(_.image.contains(entry)).get + //This may look complicated but essentially we see wether the argumnets of a predicate and the corresponding entry match + val viperPred = InterpreterCache.getPreds().filter(p => p.formalArgs.map(x => symbolConv.toSort(x.typ)).zip(corr_function.argtypes).find(x => x._1 != x._2).isEmpty && + {val gop = InterpreterCache.getGobraPreds().find(x => p.name.startsWith(x.id.name)) + gop.isDefined && gop.get.args.drop(corr_function.argtypes.size).map(InterpreterCache.getType(_)).zip(info.args).find(x => x._1 != x._2).isEmpty + } + ) + val gobraPred = InterpreterCache.getGobraPreds().filter(x => viperPred.find(_.name.startsWith(x.id.name)).isDefined) + val args = corr_function.options.find(_._2 == entry) match { + case Some(x) => if(gobraPred.size >= 1) + Some(x._1.zip(gobraPred.head.args.map(InterpreterCache.getType(_))).map((x => MasterInterpreter(c).interpret(x._1, x._2).asInstanceOf[LitEntry]))) + else + None + case _ => if (gobraPred.size >= 1) + Some(gobraPred.head.args.dropRight(info.args.size).zipWithIndex.map(x => UnknownValueButKnownType(s"?", InterpreterCache.getType(x._1)))) + else + None + } + + FCPredicate(if(gobraPred.size == 1) gobraPred.head.id.name else gobraPred.map(_.id.name).mkString("/"), + args, info.args) + + }else{ + FaultEntry("Predicate domain not found") + } + } +} + +case class UserDomainInterpreter(c: sil.Converter) extends GobraDomainInterpreter[DeclaredT] { //TODO: maybe also return the translated domain? + def interpret(entry: sil.DomainValueEntry, info: DeclaredT): GobraModelEntry = { + val original = UserDomainEntry(info.decl.left.name, entry.id) + if(InterpreterCache.existsDomain(original)) return original + InterpreterCache.addDomain(original) + val domainType = info.context.symbType(info.decl.right) match{ + case t: DomainT => t + case _ => return FaultEntry("tried to interpret non domain type") + } + val viperdomain = c.domains.find(_.valueName == entry.domain) + + val funcs = translateFuncs(domainType.decl.funcs, viperdomain.get.functions, info.context) + + val relevantFuncs = funcs.filter(_.argTypes == Seq(info)) + + ExtendedUserDomainEntry(original, relevantFuncs) + } + def translateFuncs(funcDecl: Vector[PDomainFunction], viperFuncs: Seq[sil.ExtractedFunction], info: ExternalTypeInfo): Vector[FunctionEntry] = { + val corr_funcs = funcDecl.map(f => (f, viperFuncs.find(_.fname.startsWith(f.id.name)))).collect({case (x, Some(y)) => (x, y)}) + val functions = corr_funcs.map(x => translateFunc(x._1, x._2, info)) + functions + } + def translateFunc(funcDecl: PDomainFunction, viperFunc: sil.ExtractedFunction, info: ExternalTypeInfo): FunctionEntry = { + val fname = funcDecl.id.name + val argTypes = funcDecl.args.map(Util.getType(_, info)) + val resType = Util.getType(funcDecl.result, info) + val options = viperFunc.options.map(x => + (x._1.zip(argTypes).map(y => MasterInterpreter(c).interpret(y._1, y._2)), + MasterInterpreter(c).interpret(x._2, resType)) + ) + val default = MasterInterpreter(c).interpret(viperFunc.default, resType) + FunctionEntry(fname, argTypes, resType, options, default) + } + +} + diff --git a/src/main/scala/viper/gobra/reporting/VerifierError.scala b/src/main/scala/viper/gobra/reporting/VerifierError.scala index 03efcc6a2..6a95cc402 100644 --- a/src/main/scala/viper/gobra/reporting/VerifierError.scala +++ b/src/main/scala/viper/gobra/reporting/VerifierError.scala @@ -10,6 +10,7 @@ import viper.gobra.ast.frontend import viper.gobra.ast.frontend.{PReceive, PSendStmt} import viper.gobra.util.Violation.violation import viper.silver.ast.SourcePosition +import viper.silver.verifier.Counterexample sealed trait VerifierError { def position: Option[SourcePosition] @@ -60,12 +61,13 @@ sealed trait VerificationError extends VerifierError { def localMessage: String override def id: String = (localId :: reasons.map(_.id)).mkString(":") + var counterexample : Option[GobraCounterexample] = None override def message: String = { val reasonsMsg = if (reasons.nonEmpty) s"\n${reasons.mkString("\n")}" else "" val detailsMsg = if (details.nonEmpty) s"\n${details.mkString("\n")}" else "" - - s"$localMessage. $reasonsMsg$detailsMsg" + val counterexampleMsg = counterexample match { case None => "" case Some(ce)=> s"\nPossible counterexample:\n${ce.toString()}"} + s"$localMessage. $reasonsMsg$detailsMsg.$counterexampleMsg" } protected var _reasons: List[VerificationErrorReason] = List.empty diff --git a/src/main/scala/viper/gobra/translator/Names.scala b/src/main/scala/viper/gobra/translator/Names.scala index d065bc854..e315bab4a 100644 --- a/src/main/scala/viper/gobra/translator/Names.scala +++ b/src/main/scala/viper/gobra/translator/Names.scala @@ -61,6 +61,7 @@ object Names { // struct def sharedStructDomain: String = "ShStruct" def sharedStructDfltFunc: String = "shStructDefault" + def getterFunc(i:Int,arity:Int): String = s"get${i}of$arity" // types def typesDomain: String = "Types" @@ -71,6 +72,10 @@ object Names { def sharedArrayDomain: String = "ShArray" def arrayConversionFunc: String = "arrayConversion" def arrayDefaultFunc: String = "arrayDefault" + def location(domain: String) = s"${domain}loc" // function ShArrayloc(a: ShArray[T], i: Int): T + def length(domain: String) = s"${domain}len" // function ShArraylen(a: ShArray[T]): Int + def first(domain: String) = s"${domain}first" // function ShArrayfirst(r: T): ShArray[T] + def second(domain: String) = s"${domain}second" // function ShArraysecond(r: T): Int // slices def fullSliceFromArray: String = "sfullSliceFromArray" @@ -79,6 +84,10 @@ object Names { def sliceDefaultFunc: String = "sliceDefault" def sliceFromArray: String = "ssliceFromArray" def sliceFromSlice: String = "ssliceFromSlice" + def sliceArray :String = "sarray" //function sarray(s: Slice[T]): ShArray[T] + def sliceOffset :String = "soffset" // function soffset(s: Slice[T]): Int + def sliceLength :String = length("s") // function slen(s: Slice[T]): Int + def sliceCapacity :String = "scap" //function scap(s: Slice[T]): Int // sequences def emptySequenceFunc: String = "sequenceEmpty" @@ -96,6 +105,17 @@ object Names { // built-in members def builtInMember: String = "built_in" + //strings + def stringLength: String = "strLen" // function strLen(id: Int): Int ---- ? TODO: possibly make this Stinglen aka length("String")? + def stringConact: String = "strConcat" // function strConcat(l: Int, r: Int): Int + def stringPrefix: String = "stringLit" + + + //options TODO: maybe extract "opt" + def optionSome: String = "optSome" //function optSome(e: T): Option[T] + def optionNone: String = "optNone" //function optNone(): Option[T] + def optionGet : String = "optGet" //function optGet(o: Option[T]): T + def optionIsNone:String= "optIsNone" //function optIsNone(o: Option[T]): Bool // ints def bitwiseAnd: String = "intBitwiseAnd" def bitwiseOr: String = "intBitwiseOr" diff --git a/src/main/scala/viper/gobra/translator/Translator.scala b/src/main/scala/viper/gobra/translator/Translator.scala index 97e086422..775306173 100644 --- a/src/main/scala/viper/gobra/translator/Translator.scala +++ b/src/main/scala/viper/gobra/translator/Translator.scala @@ -6,7 +6,8 @@ package viper.gobra.translator - +import viper.gobra.reporting.BackTranslator.VerificationBackTrackInfo +import viper.silver.{ast => vpr} import viper.gobra.ast.internal.Program import viper.gobra.backend.BackendVerifier import viper.gobra.frontend.Config @@ -18,11 +19,13 @@ import viper.gobra.util.Violation object Translator { - def translate(program: Program)(config: Config): BackendVerifier.Task = { + def translate(program: Program)(config: Config,typeInfo:viper.gobra.frontend.info.TypeInfo): BackendVerifier.Task = { val translationConfig = new DfltTranslatorConfig() val programTranslator = new ProgramsImpl() - val task = programTranslator.translate(program)(translationConfig) - + val task1 = programTranslator.translate(program)(translationConfig) + val task = BackendVerifier.Task(task1.program,task1.backtrack.copy(config=config,typeInfo=typeInfo)) + //TODO: resolve this merge conflict + if (config.checkConsistency) { val errors = task.program.checkTransitively if (errors.nonEmpty) Violation.violation(errors.toString) @@ -35,10 +38,11 @@ object Translator { val transformedTask = transformers.foldLeft(task) { case (t, transformer) => transformer.transform(t) - } + } config.reporter report GeneratedViperMessage(config.inputFiles.head, () => transformedTask.program, () => transformedTask.backtrack) transformedTask + } } diff --git a/src/main/scala/viper/gobra/translator/implementations/translator/ProgramsImpl.scala b/src/main/scala/viper/gobra/translator/implementations/translator/ProgramsImpl.scala index 36b693041..aee6af8ca 100644 --- a/src/main/scala/viper/gobra/translator/implementations/translator/ProgramsImpl.scala +++ b/src/main/scala/viper/gobra/translator/implementations/translator/ProgramsImpl.scala @@ -14,6 +14,7 @@ import viper.gobra.translator.interfaces.TranslatorConfig import viper.gobra.translator.interfaces.translator.Programs import viper.gobra.translator.util.ViperWriter.MemberWriter import viper.gobra.util.Violation +import viper.gobra.reporting.BackTranslator.VerificationBackTrackInfo import viper.silver.{ast => vpr} class ProgramsImpl extends Programs { @@ -78,11 +79,9 @@ class ProgramsImpl extends Programs { val (error, _, prog) = progW.execute - val backTrackInfo = BackTrackInfo(error.errorT, error.reasonT) + val backTrackInfo = BackTrackInfo(error.errorT, error.reasonT,prog,null,null) //config is added as needed, but typeInfo is missing (resolved in Translator) - BackendVerifier.Task( - program = prog, - backtrack = backTrackInfo - ) + + BackendVerifier.Task(prog,backTrackInfo) } } diff --git a/src/main/scala/viper/gobra/translator/interfaces/translator/Programs.scala b/src/main/scala/viper/gobra/translator/interfaces/translator/Programs.scala index 9b20b8231..72c37807f 100644 --- a/src/main/scala/viper/gobra/translator/interfaces/translator/Programs.scala +++ b/src/main/scala/viper/gobra/translator/interfaces/translator/Programs.scala @@ -12,4 +12,4 @@ import viper.gobra.translator.interfaces.TranslatorConfig trait Programs { def translate(program: in.Program)(conf: TranslatorConfig): BackendVerifier.Task -} +} \ No newline at end of file diff --git a/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala b/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala index 89787c87c..6d0f54eda 100644 --- a/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala +++ b/src/test/scala/viper/gobra/DetailedBenchmarkTests.scala @@ -18,6 +18,7 @@ import viper.gobra.frontend.info.{Info, TypeInfo} import viper.gobra.frontend.{Desugar, Parser} import viper.gobra.reporting.{AppliedInternalTransformsMessage, BackTranslator, VerifierError, VerifierResult} import viper.gobra.translator.Translator +import viper.silver.{ast=>vpr} import scala.concurrent.Await import scala.concurrent.duration.Duration @@ -90,7 +91,7 @@ class DetailedBenchmarkTests extends BenchmarkTests { // however, as we will directly invoke the individual steps of Gobra, we have to manually merge in-file configs // such that the Gobra programs show the same behavior as when invoking `Gobra.verify`: assert(config.isDefined) - config = Some(gobra.getAndMergeInFileConfig(config.get)) + config = Some(gobra.getAndMergeInFileConfig(config.get))//.copy(counterexample=Some(viper.gobra.reporting.CounterexampleConfigs.MappedCounterexamples))) } private val parsing = InitialStep("parsing", () => { @@ -105,38 +106,47 @@ class DetailedBenchmarkTests extends BenchmarkTests { Info.check(parsedPackage)(config.get).map(typeInfo => (parsedPackage, typeInfo)) }) - private val desugaring: NextStep[(PPackage, TypeInfo), Program, Vector[VerifierError]] = - NextStep("desugaring", typeChecking, { case (parsedPackage: PPackage, typeInfo: TypeInfo) => + private val desugaring: NextStep[(PPackage, TypeInfo), (Program,TypeInfo), Vector[VerifierError]] = + NextStep("desugaring", typeChecking, { case (parsedPackage: PPackage, typeInfo: TypeInfo) =>{ assert(config.isDefined) - Right(Desugar.desugar(parsedPackage, typeInfo)(config.get)) - }) + Right((Desugar.desugar(parsedPackage, typeInfo)(config.get),typeInfo)) + }}) - private val internalTransforming = NextStep("internal transforming", desugaring, (program: Program) => { + private val internalTransforming : NextStep[(Program, TypeInfo), (Program,TypeInfo), Vector[VerifierError]]= NextStep("internal transforming", desugaring, { case (program: Program, typeInfo: TypeInfo) =>{ assert(config.isDefined) val c = config.get if (c.checkOverflows) { val result = OverflowChecksTransform.transform(program) c.reporter report AppliedInternalTransformsMessage(c.inputFiles.head, () => result) - Right(result) + Right((result,typeInfo)) } else { - Right(program) + Right((program,typeInfo)) } - }) + }}) - private val encoding = NextStep("Viper encoding", internalTransforming, (program: Program) => { + private val encoding:NextStep[(Program, TypeInfo), BackendVerifier.Task, Vector[VerifierError]] = NextStep("Viper encoding", internalTransforming, { case (program: Program, typeInfo: TypeInfo) =>{ assert(config.isDefined) - Right(Translator.translate(program)(config.get)) - }) + Right(Translator.translate(program)(config.get,typeInfo)) + }}) - private val verifying = NextStep("Viper verification", encoding, (viperTask: BackendVerifier.Task) => { + private val verifying : NextStep[BackendVerifier.Task,BackendVerifier.Result , Vector[VerifierError]] = NextStep("Viper verification", encoding, { case viperTask:BackendVerifier.Task => + assert(config.isDefined) val c = config.get val resultFuture = BackendVerifier.verify(viperTask)(c)(executor) - .map(BackTranslator.backTranslate(_)(c))(executor) + Right(Await.result(resultFuture, Duration(timeoutSec, TimeUnit.SECONDS))) }) + // added for convenience + private val backtranslate : NextStep[BackendVerifier.Result,VerifierResult , Vector[VerifierError]] = NextStep("Backtranslation", verifying, { case viperResult:BackendVerifier.Result => + + assert(config.isDefined) + val c = config.get + Right(BackTranslator.backTranslate(viperResult)(c)) + + }) - private val lastStep = verifying + private val lastStep = backtranslate /** Phases of the frontend which are executed sequentially. */ override val phases: Seq[Phase] = lastStep.phases diff --git a/src/test/scala/viper/gobra/counterexample/CounterexmpleUnitTest.scala b/src/test/scala/viper/gobra/counterexample/CounterexmpleUnitTest.scala new file mode 100644 index 000000000..503ca9852 --- /dev/null +++ b/src/test/scala/viper/gobra/counterexample/CounterexmpleUnitTest.scala @@ -0,0 +1,99 @@ +import viper.silicon.{reporting => sil} +import viper.gobra.reporting._ +import viper.gobra.frontend.info.base.Type._ +import org.scalatest.{Assertion, Inside, Succeeded} +import org.scalatest.funsuite.AnyFunSuite +import org.scalatest.matchers.should.Matchers +import viper.gobra.util.TypeBounds +import viper.gobra.translator.Names +import viper.silicon.state.{terms => term} + +class CounterexampleUnitTests extends AnyFunSuite with Matchers with Inside { + val constFalse = sil.LitBoolEntry(false) + val constTrue =sil.LitBoolEntry(true) + val constZero = sil.LitIntEntry(0) + val intType = IntT(TypeBounds.DefaultInt) + + test("Integer"){ + testInterpreterSingle(null,sil.LitIntEntry(42),intType,LitIntEntry(42)) + } + test("String"){ + val stringId = sil.LitIntEntry(1) + val helloWorld = Names.stringPrefix ++ "68656c6c6f20776f726c64" + val func = sil.ExtractedFunction(helloWorld,Seq(),term.sorts.Int,Map(),stringId) + + val StringDomain = sil.DomainEntry(Names.stringsDomain,Seq(),Seq(func)) + val converter = new TestConverter(Seq(StringDomain),Seq(),identity(_)) + val should = LitStringEntry("hello world") + testInterpreterSingle(converter,stringId,StringT,should) + } + + test("Boolean"){ + testInterpreterSingle(null,sil.LitBoolEntry(false),BooleanT,LitBoolEntry(false)) + } + test("Integer Array"){ + val length = 10 + val values = 0.until(length) + val typ = ArrayT(length,IntT(TypeBounds.DefaultInt)) + val should = LitArrayEntry(typ,values.map(x=>LitIntEntry(x))) + val embedding = Names.embeddingDomain ++ Names.freshName + val seqName = "Seq!val!1" + val entry1 = sil.VarEntry(seqName,term.sorts.Seq(term.sorts.Int)) + val entry2 = sil.VarEntry(seqName++"0",term.sorts.Seq(term.sorts.Int)) + val boxSort = term.sorts.UserSort(viper.silicon.state.Identifier(embedding)) + val sort = term.sorts.Seq(term.sorts.Int) + val entry = sil.SeqEntry(seqName,values.map(sil.LitIntEntry(_)).toVector) + val getValEntry = (v:sil.VarEntry) => v.name match { case seqName => entry case _ => sil.NullRefEntry("Ref!val!1") } + val boxedVal = sil.DomainValueEntry(embedding,"1") + val unbox = sil.ExtractedFunction(Names.embeddingUnboxFunc++embedding, Seq(boxSort), sort, Map((Seq(boxedVal),entry1)), entry2) + val box = sil.ExtractedFunction(Names.embeddingBoxFunc++embedding, Seq(sort), boxSort, Map((Seq(entry1),boxedVal)), sil.DomainValueEntry(embedding,"0")) + val embDomain = sil.DomainEntry(embedding,Seq(),Seq()) + val converter = new TestConverter(Seq(embDomain),Seq(unbox,box),getValEntry) + + testInterpreterSingle(converter,entry1,typ,should) + } + test("Options"){ + val box = 1024 + val value = sil.LitIntEntry(box) + val domName = "Option" + val intSorts = term.sorts.Int + val concDomName = domName ++ "[Int]" + val optSort = term.sorts.UserSort(viper.silicon.state.Identifier(concDomName)) + val someVal = sil.DomainValueEntry(concDomName,"1") + val someOther = sil.DomainValueEntry(concDomName,"2") + val noneVal = sil.DomainValueEntry(concDomName,"0") + val emptymap = Map.empty[Seq[sil.ExtractedModelEntry],sil.ExtractedModelEntry] + val domfuncs = Seq( + (Names.optionNone,Seq(optSort),intSorts,emptymap,someVal), + (Names.optionIsNone,Seq(optSort),term.sorts.Bool,Map((Seq(noneVal), constTrue)),constFalse), + (Names.optionGet, Seq(optSort), intSorts, Map((Seq(someVal),value)),constZero), + (Names.optionSome, Seq(intSorts),optSort,Map((Seq(value),someVal)),someOther) + ).map(x=>sil.ExtractedFunction(x._1,x._2,x._3,x._4.asInstanceOf[Map[Seq[sil.ExtractedModelEntry],sil.ExtractedModelEntry]],x._5)) + val optionDomain = sil.DomainEntry(domName,Seq(viper.silver.ast.Int),domfuncs) + val converter = new TestConverter(Seq(optionDomain),Seq(),identity(_)) + testInterpreterSingle(converter,someVal,OptionT(intType),LitOptionEntry(Some(LitIntEntry(box)))) + testInterpreterSingle(converter,noneVal,OptionT(intType),LitOptionEntry(None)) + } + + + def testInterpreterSingle(c:sil.Converter, example:sil.ExtractedModelEntry,typ:Type,expectedOutput:GobraModelEntry): Unit = { + val produced = MasterInterpreter(c).interpret(example,typ) + assert( produced == expectedOutput ,s"Should be: $expectedOutput, but got: $produced") + } + + def testFile(path:String,expected:GobraCounterexample): Boolean ={ + false + } + + def mkConverter() :sil.Converter ={ + new TestConverter(null,null,null) + } +} + +class TestConverter(doms:Seq[sil.DomainEntry],functions:Seq[sil.ExtractedFunction],extractValnew:(sil.VarEntry => sil.ExtractedModelEntry)) extends sil.Converter(null,null,null,null,null) { + override lazy val non_domain_functions = functions + override lazy val domains = doms + override def extractVal(x:sil.VarEntry) = extractValnew(x) +} + +