Unable to install under Ubuntu 18.04: Failed to read artifact descriptor for com.runtimeverification.rv_match:ocaml-backend:jar:1.0-SNAPSHOT

[practicalswift]

When installing and testing kcc under Ubuntu 18.04 LTS I encounter the following two errors:

$ mvn dependency:copy -Dartifact=com.runtimeverification.rv_match:ocaml-backend:1.0-SNAPSHOT -DoutputDirectory=k-distribution/target/release/k/lib/java
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-dependency-plugin:3.1.1:copy (default-cli) on project parent: Unable to find/resolve artifact.: Failed to read artifact descriptor for com.runtimeverification.rv_match:ocaml-backend:jar:1.0-SNAPSHOT: Failure to find com.runtimeverification.rv_match:parent:pom:1.0-SNAPSHOT in https://s3.us-east-2.amazonaws.com/runtimeverificationmaven/snapshots was cached in the local repository, resolution will not be reattempted until the update interval of runtime.verification.snapshots has elapsed or updates are forced -> [Help 1]

$ kcc -o test test.c
$ ./test
[Error] Critical: Kompiled definition is out of date with the latest version of
the K tool. Please re-run kompile and try again.
(org.kframework.attributes.Att; local class incompatible: stream classdesc
serialVersionUID = 7821041571729343693, local class serialVersionUID =
4421725027641465071)

I guess the latter error is a consequence of the first error, but so far I've been unable to resolve it.

Likely I'm missing something obvious here: what am I doing wrong? :-)

Full log:

$ cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=18.04
DISTRIB_CODENAME=bionic
DISTRIB_DESCRIPTION="Ubuntu 18.04.2 LTS"
$ git clone https://github.com/runtimeverification/k.git
$ cd k
$ git rev-parse HEAD
ae65bb5a834cb7f26dcfa4358fc02ef6b3bccd55
$ git submodule update --init --recursive
$ llvm-backend/src/main/native/llvm-backend/install-rust
$ mvn package
…
[INFO] ------------------------------------------------------------------------
[INFO] Reactor Summary for K Framework Tool Parent 1.0-SNAPSHOT:
[INFO]
[INFO] K Framework Tool Parent ............................ SUCCESS [  0.777 s]
[INFO] K Framework KORE ................................... SUCCESS [01:12 min]
[INFO] K Framework Tool Kernel ............................ SUCCESS [ 28.023 s]
[INFO] K Framework KTree .................................. SUCCESS [  0.261 s]
[INFO] K Framework Ocaml Backend .......................... SUCCESS [  1.167 s]
[INFO] K Framework Java Backend ........................... SUCCESS [  6.052 s]
[INFO] K Framework Haskell Backend ........................ SUCCESS [08:00 min]
[INFO] K Framework LLVM Backend Pattern Matching .......... SUCCESS [ 14.594 s]
[INFO] K Framework LLVM Backend ........................... SUCCESS [ 30.781 s]
[INFO] K Framework Tool Distribution ...................... SUCCESS [ 35.948 s]
[INFO] ------------------------------------------------------------------------
[INFO] BUILD SUCCESS
[INFO] ------------------------------------------------------------------------
[INFO] Total time:  11:13 min
[INFO] Finished at: 2019-05-15T13:03:18+02:00
[INFO] ------------------------------------------------------------------------
$ echo $?
0
$ export PATH=$(pwd)/k-distribution/target/release/k/bin:$PATH
$ krun --version
RV-K version 1.0-SNAPSHOT
Git revision: ae65bb5
Git branch: master
Build date: Wed May 15 12:53:22 CEST 2019
$ kompile --version
RV-K version 1.0-SNAPSHOT
Git revision: ae65bb5
Git branch: master
Build date: Wed May 15 12:53:22 CEST 2019
$ mvn dependency:copy -Dartifact=com.runtimeverification.rv_match:ocaml-backend:1.0-SNAPSHOT -DoutputDirectory=k-distribution/target/release/k/lib/java
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/usr/share/maven/lib/guice.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of com.google.inject.internal.cglib.core.$ReflectUtils$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
[INFO] Scanning for projects...
[INFO] ------------------------------------------------------------------------
[INFO] Reactor Build Order:
[INFO]
[INFO] K Framework Tool Parent                                            [pom]
[INFO] K Framework KORE                                                   [jar]
[INFO] K Framework Tool Kernel                                            [jar]
[INFO] K Framework KTree                                                  [jar]
[INFO] K Framework Ocaml Backend                                          [jar]
[INFO] K Framework Java Backend                                           [jar]
[INFO] K Framework Haskell Backend                                        [jar]
[INFO] K Framework LLVM Backend Pattern Matching                          [jar]
[INFO] K Framework LLVM Backend                                           [jar]
[INFO] K Framework Tool Distribution                                      [jar]
[INFO]
[INFO] ------------------< com.runtimeverification.k:parent >------------------
[INFO] Building K Framework Tool Parent 1.0-SNAPSHOT                     [1/10]
[INFO] --------------------------------[ pom ]---------------------------------
[INFO]
[INFO] --- maven-dependency-plugin:3.1.1:copy (default-cli) @ parent ---
[INFO] Configured Artifact: com.runtimeverification.rv_match:ocaml-backend:1.0-SNAPSHOT:jar
[INFO] ------------------------------------------------------------------------
[INFO] Reactor Summary for K Framework Tool Parent 1.0-SNAPSHOT:
[INFO]
[INFO] K Framework Tool Parent ............................ FAILURE [  1.774 s]
[INFO] K Framework KORE ................................... SKIPPED
[INFO] K Framework Tool Kernel ............................ SKIPPED
[INFO] K Framework KTree .................................. SKIPPED
[INFO] K Framework Ocaml Backend .......................... SKIPPED
[INFO] K Framework Java Backend ........................... SKIPPED
[INFO] K Framework Haskell Backend ........................ SKIPPED
[INFO] K Framework LLVM Backend Pattern Matching .......... SKIPPED
[INFO] K Framework LLVM Backend ........................... SKIPPED
[INFO] K Framework Tool Distribution ...................... SKIPPED
[INFO] ------------------------------------------------------------------------
[INFO] BUILD FAILURE
[INFO] ------------------------------------------------------------------------
[INFO] Total time:  4.986 s
[INFO] Finished at: 2019-05-15T13:13:44+02:00
[INFO] ------------------------------------------------------------------------
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-dependency-plugin:3.1.1:copy (default-cli) on project parent: Unable to find/resolve artifact.: Failed to read artifact descriptor for com.runtimeverification.rv_match:ocaml-backend:jar:1.0-SNAPSHOT: Failure to find com.runtimeverification.rv_match:parent:pom:1.0-SNAPSHOT in https://s3.us-east-2.amazonaws.com/runtimeverificationmaven/snapshots was cached in the local repository, resolution will not be reattempted until the update interval of runtime.verification.snapshots has elapsed or updates are forced -> [Help 1]
[ERROR]
[ERROR] To see the full stack trace of the errors, re-run Maven with the -e switch.
[ERROR] Re-run Maven using the -X switch to enable full debug logging.
[ERROR]
[ERROR] For more information about the errors and possible solutions, please read the following articles:
[ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/MojoExecutionException
$ git clone --depth=1 https://github.com/kframework/c-semantics.git
$ k-configure-opam-dev
$ eval `opam config env`
$ cd c-semantics
$ git rev-parse HEAD
917425f62c344911b2c0d03f40112a47b326137d
$ make -j$(nproc)
$ make check
$ export PATH=$PATH:$(pwd)/dist
$ cd ..
$ cat test.c
int main(void) {
    int i = 1;
    i += 1;
    return i;
}
$ kcc -o test test.c
$ ./test
[Error] Critical: Kompiled definition is out of date with the latest version of
the K tool. Please re-run kompile and try again.
(org.kframework.attributes.Att; local class incompatible: stream classdesc
serialVersionUID = 7821041571729343693, local class serialVersionUID =
4421725027641465071)

[chathhorn]

It looks like our install/build instructions are out-of-date. Can you try this:

$ sudo apt-get install bison clang++-6.0 clang-6.0 cmake make coreutils \
        diffutils flex libboost-test-dev libffi-dev libgmp-dev libjemalloc-dev libmpfr-dev \
        gcc-5 libstdc++6 g++-5 libyaml-cpp-dev llvm-6.0 m4 opam git \
        pkg-config python3 unifdef zlib1g-dev openjdk-8-jdk maven \
        libuuid-tiny-perl libstring-escape-perl libstring-shellquote-perl \
        libgetopt-declare-perl libapp-fatpacker-perl
$ git clone --depth=1 https://github.com/kframework/c-semantics.git
$ cd c-semantics
$ make -j4
$ export PATH=$PATH:`pwd`/dist

Let me know if that works for you and I'll update the install instructions.

Also, we have binary releases of RV-Match, which is basically the open source version here extended with some more features, available here (for Ubuntu 18.04 and 16.04): https://github.com/runtimeverification/match/releases

[practicalswift]

@chathhorn Thanks! That takes me slightly longer :-)

$ sudo apt-get install bison clang++-6.0 clang-6.0 cmake make coreutils \
        diffutils flex libboost-test-dev libffi-dev libgmp-dev libjemalloc-dev libmpfr-dev \
        gcc-5 libstdc++6 g++-5 libyaml-cpp-dev llvm-6.0 m4 opam git \
        pkg-config python3 unifdef zlib1g-dev openjdk-8-jdk maven \
        libuuid-tiny-perl libstring-escape-perl libstring-shellquote-perl \
        libgetopt-declare-perl libapp-fatpacker-perl
$ git clone --depth=1 https://github.com/kframework/c-semantics.git
$ cd c-semantics
$ make -j $(nproc)
$ echo $?
0
$ export PATH=$PATH:$(pwd)/dist
$ cd
$ kcc --version

        kcc: version 1.0 GNU-compatible

        Current profile: x86-gcc-limited-libc
        Installed profiles: x86-gcc-limited-libc
        Default profile: x86-gcc-limited-libc

        To request additional profiles, contact runtimeverification.com/support.

$ k++ --version

        k++: version 1.0 GNU-compatible

        Current profile: x86-gcc-limited-libc
        Installed profiles: x86-gcc-limited-libc
        Default profile: x86-gcc-limited-libc

        To request additional profiles, contact runtimeverification.com/support.

$ kcc -o test test.c
$ ./test
Can't exec "krun": No such file or directory at ./test line 153.

Am I missing some PATH requirement?

[chathhorn]

Yeah, oops:

$ export PATH=$PATH:$(pwd)/.build/k/k-distribution/target/release/k/bin

Where pwd is the c-semantics repository root.

[practicalswift]

Thanks! Now it seems to work.

$ cat pointer.c
#include <string.h>

int main(void) {
  char foo[1] = {0};
  void* one_past_end = foo + sizeof(foo);
  memset(one_past_end, 0, 0);
}
$ kcc -o pointer pointer.c && ./pointer
$ ~/tis-interpreter/tis-interpreter.sh pointer.c
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
pointer.c:6:[value] warning: invalid pointer {{ &foo + {1} }}: the pointer must be valid
                 even though the size is zero.
                 assert(one_past_end is a valid pointer for writing)
                 stack: memset :: pointer.c:6 <- main
[value] done for function main

(I'm not sure if tis-interpreter or kcc is more correct above! :-))

[chathhorn]

There's some discussion of this here: https://stackoverflow.com/questions/45350528/strncpyd-s-0-with-one-past-pointer

I'd say it's probably well-defined -- a pointer to one past an object, at least, is usually considered perfectly valid. But there's clearly some ambiguity in the standard here, so kcc should probably flag this case as well.

[practicalswift]

Yes, I guess it boils down to if memset requires the pointer to be valid (which one_past_end is) or valid for writing (which one_past_end isn't) :-)