search

vmware / differential-datalog

DDlog is a programming language for incremental computation. It is well suited for writing programs that continuously update their output in response to input changes. A DDlog programmer does not write incremental algorithms; instead they specify the desired input-output mapping in a declarative manner.
MIT License
1.38k stars 118 forks source link

"Error: cannot convert -4 to u32" (via Souffle translator) #241

Closed gfour closed 5 years ago

gfour commented 5 years ago

The problem: running a Datalog analysis in Doop with DDlog fails with this error:

Error: cannot convert -4 to u32

I don't know if the error comes from subtraction or overflowing addition but there seems to be a misrepresentation of signed integers as unsigned ones. For example, in this test Souffle program:

.decl X(n: number)
.output X

X(10).
X(-1).

the souffle.dump output shows -1 as the maximum 32-bit unsigned integer:

RX{10}
RX{4294967295}

You can test it via Doop:

export DDLOG_DIR=path/to/differential-datalog
./doop -i http://centauri.di.uoa.gr:8081/artifactory/Demo-benchmarks/test-resources/006-hello-world-1.2.jar -a micro --id hello-world --Xstats-none --via-ddlog -Ldebug
gfour commented 5 years ago

I am also attaching the analysis logic.

gen_1272258801802673380.dl.zip

ryzhyk commented 5 years ago

Thanks for reporting. As a matter of fact, we are working on adding proper support for signed integers to both DDlog and the souffle-to-ddlog converter right now. We'll try to get it to a state that will be enough to unblock you today.

mihaibudiu commented 5 years ago

Once merged this PR will provide support for negative literals: https://github.com/ryzhyk/differential-datalog/pull/238

ryzhyk commented 5 years ago

@gfour, I get this error when running Doop. Any idea how to get around it?

./doop -i http://centauri.di.uoa.gr:8081/artifactory/Demo-benchmarks/test-resources/006-hello-world-1.2.jar -a micro --id hello-world --Xstats-none --via-ddlog -Ldebug
> Task :generateGrammarSource FAILED

FAILURE: Build failed with an exception.

* What went wrong:
Could not resolve all files for configuration ':antlr'.
> Could not resolve org.antlr:antlr4:4.5.1-1.
  Required by:
      project :
   > Could not resolve org.antlr:antlr4:4.5.1-1.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/org/antlr/antlr4/4.5.1-1/antlr4-4.5.1-1.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/org/antlr/antlr4/4.5.1-1/antlr4-4.5.1-1.pom'.
            > Connection reset
   > Could not resolve org.antlr:antlr4:4.5.1-1.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/org/antlr/antlr4/4.5.1-1/antlr4-4.5.1-1.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/org/antlr/antlr4/4.5.1-1/antlr4-4.5.1-1.pom'.
            > Connection reset
   > Could not resolve org.antlr:antlr4:4.5.1-1.
      > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/org/antlr/antlr4/4.5.1-1/antlr4-4.5.1-1.pom'.
         > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/org/antlr/antlr4/4.5.1-1/antlr4-4.5.1-1.pom'. Received status code 400 from server: Repository version policy: SNAPSHOT does not allow version: 4.5.1-1

* Try:
Run with --stacktrace option to get the stack trace. Run with --info or --debug option to get more log output. Run with --scan to get full insights.

* Get more help at https://help.gradle.org
gfour commented 5 years ago

@ryzhyk This sounds like a temporary network error with fetching dependencies via our own repo front end. I couldn't reproduce it but I added an explicit upstream repo to our build file. Can you pull the latest version of Doop and try again?

ryzhyk commented 5 years ago

@gfour , thanks, it made some progress, but now I get more of the same:

> Could not resolve org.clyze:clue-common:3.8.41.
  Required by:
      project :
   > Could not resolve org.clyze:clue-common:3.8.41.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/org/clyze/clue-common/3.8.41/clue-common-3.8.41.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/org/clyze/clue-common/3.8.41/clue-common-3.8.41.pom'.
            > Connection reset
   > Could not resolve org.clyze:clue-common:3.8.41.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/org/clyze/clue-common/3.8.41/clue-common-3.8.41.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/org/clyze/clue-common/3.8.41/clue-common-3.8.41.pom'.
            > Connection reset
   > Could not resolve org.clyze:clue-common:3.8.41.
      > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/org/clyze/clue-common/3.8.41/clue-common-3.8.41.pom'.
         > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/org/clyze/clue-common/3.8.41/clue-common-3.8.41.pom'. Received status code 400 from server: Repository version policy: SNAPSHOT does not allow version: 3.8.41
> Could not resolve org.clyze:deepdoop:0.9.2.
  Required by:
      project :
   > Could not resolve org.clyze:deepdoop:0.9.2.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/org/clyze/deepdoop/0.9.2/deepdoop-0.9.2.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/org/clyze/deepdoop/0.9.2/deepdoop-0.9.2.pom'.
            > Connection reset
   > Could not resolve org.clyze:deepdoop:0.9.2.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/org/clyze/deepdoop/0.9.2/deepdoop-0.9.2.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/org/clyze/deepdoop/0.9.2/deepdoop-0.9.2.pom'.
            > Connection reset
   > Could not resolve org.clyze:deepdoop:0.9.2.
      > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/org/clyze/deepdoop/0.9.2/deepdoop-0.9.2.pom'.
         > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/org/clyze/deepdoop/0.9.2/deepdoop-0.9.2.pom'. Received status code 400 from server: Repository version policy: SNAPSHOT does not allow version: 0.9.2
> Could not resolve com.github.plast-lab:HeapDL:1.0.2.
  Required by:
      project :
   > Could not resolve com.github.plast-lab:HeapDL:1.0.2.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/com/github/plast-lab/HeapDL/1.0.2/HeapDL-1.0.2.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/com/github/plast-lab/HeapDL/1.0.2/HeapDL-1.0.2.pom'.
            > Connection reset
   > Could not resolve com.github.plast-lab:HeapDL:1.0.2.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/com/github/plast-lab/HeapDL/1.0.2/HeapDL-1.0.2.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/com/github/plast-lab/HeapDL/1.0.2/HeapDL-1.0.2.pom'.
            > Connection reset
   > Could not resolve com.github.plast-lab:HeapDL:1.0.2.
      > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/com/github/plast-lab/HeapDL/1.0.2/HeapDL-1.0.2.pom'.
         > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/com/github/plast-lab/HeapDL/1.0.2/HeapDL-1.0.2.pom'. Received status code 400 from server: Repository version policy: SNAPSHOT does not allow version: 1.0.2
> Could not resolve ext:sootclasses:3.1.0.MINIMAL.
  Required by:
      project :
   > Could not resolve ext:sootclasses:3.1.0.MINIMAL.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/sootclasses/3.1.0.MINIMAL/sootclasses-3.1.0.MINIMAL.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/sootclasses/3.1.0.MINIMAL/sootclasses-3.1.0.MINIMAL.pom'.
            > Connection reset
   > Could not resolve ext:sootclasses:3.1.0.MINIMAL.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/sootclasses/3.1.0.MINIMAL/sootclasses-3.1.0.MINIMAL.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/sootclasses/3.1.0.MINIMAL/sootclasses-3.1.0.MINIMAL.pom'.
            > Connection reset
   > Could not resolve ext:sootclasses:3.1.0.MINIMAL.
      > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/ext/sootclasses/3.1.0.MINIMAL/sootclasses-3.1.0.MINIMAL.pom'.
         > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/ext/sootclasses/3.1.0.MINIMAL/sootclasses-3.1.0.MINIMAL.pom'. Received status code 400 from server: Repository version policy: SNAPSHOT does not allow version: 3.1.0.MINIMAL
> Could not resolve ext:AXMLPrinter:2.0.
  Required by:
      project :
   > Could not resolve ext:AXMLPrinter:2.0.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/AXMLPrinter/2.0/AXMLPrinter-2.0.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/AXMLPrinter/2.0/AXMLPrinter-2.0.pom'.
            > Connection reset
   > Could not resolve ext:AXMLPrinter:2.0.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/AXMLPrinter/2.0/AXMLPrinter-2.0.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/AXMLPrinter/2.0/AXMLPrinter-2.0.pom'.
            > Connection reset
   > Could not resolve ext:AXMLPrinter:2.0.
      > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/ext/AXMLPrinter/2.0/AXMLPrinter-2.0.pom'.
         > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/ext/AXMLPrinter/2.0/AXMLPrinter-2.0.pom'. Received status code 400 from server: Repository version policy: SNAPSHOT does not allow version: 2.0
> Could not resolve ext:soot-infoflow:2.5.1.
  Required by:
      project :
   > Could not resolve ext:soot-infoflow:2.5.1.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/soot-infoflow/2.5.1/soot-infoflow-2.5.1.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/soot-infoflow/2.5.1/soot-infoflow-2.5.1.pom'.
            > Connection reset
   > Could not resolve ext:soot-infoflow:2.5.1.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/soot-infoflow/2.5.1/soot-infoflow-2.5.1.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/soot-infoflow/2.5.1/soot-infoflow-2.5.1.pom'.
            > Connection reset
   > Could not resolve ext:soot-infoflow:2.5.1.
      > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/ext/soot-infoflow/2.5.1/soot-infoflow-2.5.1.pom'.
         > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/ext/soot-infoflow/2.5.1/soot-infoflow-2.5.1.pom'. Received status code 400 from server: Repository version policy: SNAPSHOT does not allow version: 2.5.1
> Could not resolve ext:soot-infoflow-android:2.5.1.
  Required by:
      project :
   > Could not resolve ext:soot-infoflow-android:2.5.1.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/soot-infoflow-android/2.5.1/soot-infoflow-android-2.5.1.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/soot-infoflow-android/2.5.1/soot-infoflow-android-2.5.1.pom'.
            > Connection reset
   > Could not resolve ext:soot-infoflow-android:2.5.1.
      > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/soot-infoflow-android/2.5.1/soot-infoflow-android-2.5.1.pom'.
         > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/soot-infoflow-android/2.5.1/soot-infoflow-android-2.5.1.pom'.
            > Connection reset
   > Could not resolve ext:soot-infoflow-android:2.5.1.
      > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/ext/soot-infoflow-android/2.5.1/soot-infoflow-android-2.5.1.pom'.
         > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-snapshot/ext/soot-infoflow-android/2.5.1/soot-infoflow-android-2.5.1.pom'. Received status code 400 from server: Repository version policy: SNAPSHOT does not allow version: 2.5.1
> Could not resolve ext:com.ibm.wala.util:1.5.1-SNAPSHOT.
  Required by:
      project :
   > Could not resolve ext:com.ibm.wala.util:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.util:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.util:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml'. Received status code 400 from server: Repository version policy: RELEASE does not allow metadata in path: ext/com.ibm.wala.util/1.5.1-SNAPSHOT/maven-metadata.xml
> Could not resolve ext:com.ibm.wala.core:1.5.1-SNAPSHOT.
  Required by:
      project :
   > Could not resolve ext:com.ibm.wala.core:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.core:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.core:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml'. Received status code 400 from server: Repository version policy: RELEASE does not allow metadata in path: ext/com.ibm.wala.core/1.5.1-SNAPSHOT/maven-metadata.xml
> Could not resolve ext:com.ibm.wala.shrike:1.5.1-SNAPSHOT.
  Required by:
      project :
   > Could not resolve ext:com.ibm.wala.shrike:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.shrike:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.shrike:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml'. Received status code 400 from server: Repository version policy: RELEASE does not allow metadata in path: ext/com.ibm.wala.shrike/1.5.1-SNAPSHOT/maven-metadata.xml
> Could not resolve ext:com.ibm.wala.dalvik:1.5.1-SNAPSHOT.
  Required by:
      project :
   > Could not resolve ext:com.ibm.wala.dalvik:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.dalvik:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.dalvik:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml'. Received status code 400 from server: Repository version policy: RELEASE does not allow metadata in path: ext/com.ibm.wala.dalvik/1.5.1-SNAPSHOT/maven-metadata.xml
> Could not resolve ext:com.ibm.wala.cast:1.5.1-SNAPSHOT.
  Required by:
      project :
   > Could not resolve ext:com.ibm.wala.cast:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.cast:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.cast:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml'. Received status code 400 from server: Repository version policy: RELEASE does not allow metadata in path: ext/com.ibm.wala.cast/1.5.1-SNAPSHOT/maven-metadata.xml
> Could not resolve ext:com.ibm.wala.cast.java:1.5.1-SNAPSHOT.
  Required by:
      project :
   > Could not resolve ext:com.ibm.wala.cast.java:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.cast.java:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.cast.java:1.5.1-SNAPSHOT.
      > Unable to load Maven meta-data from https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml'. Received status code 400 from server: Repository version policy: RELEASE does not allow metadata in path: ext/com.ibm.wala.cast.java/1.5.1-SNAPSHOT/maven-metadata.xml
> Could not resolve ext:com.ibm.wala.cast.python:0.0.1-SNAPSHOT.
  Required by:
      project :
   > Could not resolve ext:com.ibm.wala.cast.python:0.0.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.cast.python:0.0.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.cast.python:0.0.1-SNAPSHOT.
      > Unable to load Maven meta-data from https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml'. Received status code 400 from server: Repository version policy: RELEASE does not allow metadata in path: ext/com.ibm.wala.cast.python/0.0.1-SNAPSHOT/maven-metadata.xml
> Could not resolve ext:com.ibm.wala.cast.lsp:0.0.1-SNAPSHOT.
  Required by:
      project :
   > Could not resolve ext:com.ibm.wala.cast.lsp:0.0.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-deps/ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.cast.lsp:0.0.1-SNAPSHOT.
      > Unable to load Maven meta-data from http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'http://centauri.di.uoa.gr:8081/artifactory/plast-public/ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml'.
               > Connection reset
   > Could not resolve ext:com.ibm.wala.cast.lsp:0.0.1-SNAPSHOT.
      > Unable to load Maven meta-data from https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml.
         > Could not get resource 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml'.
            > Could not GET 'https://soot-build.cs.uni-paderborn.de/nexus/repository/soot-release/ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml'. Received status code 400 from server: Repository version policy: RELEASE does not allow metadata in path: ext/com.ibm.wala.cast.lsp/0.0.1-SNAPSHOT/maven-metadata.xml
ryzhyk commented 5 years ago

I was not able to run Doop to reproduce the problem, but it should hopefully be fixed in the latest DDlog master. Can you give it a go and let us know what happens?

gfour commented 5 years ago

The analysis no longer crashes with a negative number error, thank you for the fast fix!

ryzhyk commented 5 years ago

Great! It's a pretty complex Datalog program. Curious to know how DDlog does on it.

gfour commented 5 years ago

Great! It's a pretty complex Datalog program. Curious to know how DDlog does on it.

This analysis takes 50 sec in DDlog (vs. 11 in Souffle). These are preliminary results (still some things to verify, such as using the same subset of regex syntax between the two engines). For another measure of the work done by the analysis, here are the computed relation sizes:

Output relation         Tuples
ApplicationMethod            2
ArrayIndexPointsTo       17101
CallGraphEdge            14905
InstanceFieldPointsTo   887275
Reachable                 3328
StaticFieldPointsTo       2806
VarPointsTo            2085101
ryzhyk commented 5 years ago

Interesting, thank you! Another important parameter is memory. Because DDlog is incremental, it (or rather differential-dataflow DDlog is built upon) maintains a bunch of state in memory. This state can be fairly large and can also affect the performance due to swapping. We are currently working on some optimizations to reduce the memory footprint. Any chance you could check how much memory DDlog uses in your example (I simply use /usr/bin/time to obtain peak memory usage of the program)?

If you are using DDlog as a standalone executable rather than through an API, then parsing a large dataset and dumping the output to file could take a long time (these operations are not really super optimized).

Finally, it would be interesting to look at DDlog's CPU and memory profiles to figure out where exactly it spends time and memory. To do so, add the following command at the start of the DDlog command file: profile cpu on; and use the profile; command at the very end to dump CPU and memory profiles (these commands are documented here)

gfour commented 5 years ago

We are running analysis_cli -w 4 --no-print < in.dat &> dump and read the resulting relations from the dump file. I don't think there is any swapping happening, because the analysis runs on a machine with 200GB free RAM and 32 hardware threads. Results of running with /usr/bin/time:

94.33user 18.78system 0:51.66elapsed 218%CPU (0avgtext+0avgdata 4623960maxresident)k
0inputs+1019008outputs (0major+2361065minor)pagefaults 0swaps

Profile: profile.txt

ryzhyk commented 5 years ago

Thanks! I would also try with a different number of workers. In my experience, -w 1 or -w 2 is typically faster than -w 4.

gfour commented 5 years ago

For this program, -w 2 takes about the same time (51 sec), while -w 1 takes 63 sec.