K-user mailing list

[Christos Kloukinas <c.kloukinas AT gmail.com>]

Hi, I'm trying to install K from github.


I've tried both the UIUC & the RV versions:

https://github.com/kframework/k

https://github.com/runtimeverification/k


For both I've followed the instructions on UIUC but when I try "mvn 
package" everything builds fine apart from LLVM Backend.

The errors are mostly the same in both versions - the common files that 
are involved are:

- llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c

- llvm-backend/src/main/native/llvm-backend/runtime/alloc/collect.c

- llvm-backend/src/main/native/llvm-backend/include/runtime/header.h

- llvm-backend/src/main/native/llvm-backend/runtime/strings/strings.cpp

UIUC also has an issue with:

- 
llvm-backend/src/main/native/llvm-backend/matching/submodules/kore/src/main/haskell/kore/src/Kore/SMT/SMT.hs


I'm attaching the output of mvn package from LLVM down.


Anyone has an idea how I could proceed here?


Best,

Chris




[INFO] Building K Framework LLVM Backend 1.0-SNAPSHOT
[INFO] 
------------------------------------------------------------------------
[INFO] 
[INFO] --- maven-enforcer-plugin:3.0.0-M2:enforce 
(enforce-java) @ llvm-backend ---
[INFO] 
[INFO] --- maven-resources-plugin:2.6:resources 
(default-resources) @ llvm-backend ---
[INFO] Using 'UTF-8' encoding to copy filtered resources.
[INFO] Copying 1 resource
[INFO] 
[INFO] --- maven-compiler-plugin:3.7.0:compile 
(default-compile) @ llvm-backend ---
[INFO] Changes detected - recompiling the module!
[INFO] Compiling 4 source files to 
/opt/k/uiuc/k/llvm-backend/target/classes
[INFO] 
[INFO] --- maven-antrun-plugin:1.7:run 
(build-llvm) @ llvm-backend ---
[INFO] Executing tasks

main:
    [mkdir] Created dir: /opt/k/uiuc/k/llvm-backend/target/build
     [exec] -- The CXX compiler identification is Clang 6.0.0
     [exec] -- The C compiler identification is Clang 6.0.0
     [exec] -- Check for working CXX compiler: /usr/bin/clang++-6.0
     [exec] -- Check for working CXX compiler: /usr/bin/clang++-6.0 -- works
     [exec] -- Detecting CXX compiler ABI info
     [exec] -- Detecting CXX compiler ABI info - done
     [exec] -- Detecting CXX compile features
     [exec] -- Detecting CXX compile features - done
     [exec] -- Check for working C compiler: /usr/bin/clang-6.0
     [exec] -- Check for working C compiler: /usr/bin/clang-6.0 -- works
     [exec] -- Detecting C compiler ABI info
     [exec] -- Detecting C compiler ABI info - done
     [exec] -- Detecting C compile features
     [exec] -- Detecting C compile features - done
     [exec] -- Found LLVM 6.0.0
     [exec] -- Found ZLIB: /usr/lib/x86_64-linux-gnu/libz.so (found version 
"1.2.11") 
     [exec] -- Found BISON: /usr/bin/bison (found version "3.0.4") 
     [exec] -- Found FLEX: /usr/bin/flex (found version "2.6.4") 
     [exec] -- Found GMP: /usr/lib/x86_64-linux-gnu/libgmp.so
     [exec] -- Boost version: 1.65.1
     [exec] -- Found the following Boost libraries:
     [exec] --   unit_test_framework
     [exec] -- Configuring done
     [exec] -- Generating done
     [exec] -- Build files have been written to: 
/opt/k/uiuc/k/llvm-backend/target/build
     [exec] [  1%] [FLEX][KOREScanner] Building scanner with flex 2.6.4
     [exec] [  3%] [BISON][KOREParser] Building parser with bison 3.0.4
     [exec] Scanning/bin/sh: 1: cargo: not found
     [exec] make[2]: *** 
[runtime/datastructures/target/release/libdatastructures.rlib] Error 127
     [exec] make[1]: ***  dependencies of target matching
     [exec] Scanning dependencies of target datastructures
     [exec] [  5%] Generating bin/llvm-kompile-matching
     [exec] [  7%] Generating 
datastructures/target/release/libdatastructures.rlib
     [exec] runtime/CMakeFiles/datastructures.dir/build.make:65: recipe for 
target 'runtime/datastructures/target/release/libdatastructures.rlib' failed
     [exec] CMakeFiles/Makefile2:784: recipe for target 
'runtime/CMakeFiles/datastructures.dir/all' failed
     [exec] [runtime/CMakeFiles/datastructures.dir/all] Error 2
     [exec] make[1]: *** Waiting for unfinished jobs....
     [exec] Scanning dependencies of target arithmetic
     [exec] Scanning dependencies of target strings
     [exec] Scanning dependencies of target alloc
     [exec] [  9%] Building CXX object 
runtime/strings/CMakeFiles/strings.dir/strings.cpp.o
     [exec] [ 10%] Building CXX object 
runtime/strings/CMakeFiles/strings.dir/bytes.cpp.o
     [exec] [ 12%] Building CXX object 
runtime/arithmetic/CMakeFiles/arithmetic.dir/int.cpp.o
     [exec] [ 14%] Building C object 
runtime/alloc/CMakeFiles/alloc.dir/collect.c.o
     [exec] [ 16%] Building C object 
runtime/alloc/CMakeFiles/alloc.dir/alloc.c.o
     [exec] [ 20%] [BISON] Copying auto-generated file KOREParser.hh
     [exec] [ 20%] [BISON] Copying auto-generated file stack.hh
     [exec] [ 21%] [BISON] Copying auto-generated file location.hh
     [exec] [ 23%] [BISON] Copying auto-generated file position.hh
     [exec] Scanning dependencies of target Hello
     [exec] [ 25%] Building CXX object 
lib/hello/CMakeFiles/Hello.dir/hello.cpp.o
     [exec] Scanning dependencies of target AST
     [exec] [ 27%] Building CXX object lib/ast/CMakeFiles/AST.dir/AST.cpp.o
     [exec] Scanning dependencies of target Parser
     [exec] [ 29%] Building CXX object 
lib/parser/CMakeFiles/Parser.dir/KOREScanner.cpp.o
     [exec] [ 30%] Building CXX object 
lib/parser/CMakeFiles/Parser.dir/KOREParser.cpp.o
     [exec] [ 32%] Building CXX object 
lib/parser/CMakeFiles/Parser.dir/KOREParserDriver.cpp.o
     [exec] runtime/alloc/CMakeFiles/alloc.dir/build.make:86: recipe for 
target 'runtime/alloc/CMakeFiles/alloc.dir/collect.c.o' failed
     [exec] runtime/alloc/CMakeFiles/alloc.dir/build.make:62: recipe for 
target 'runtime/alloc/CMakeFiles/alloc.dir/alloc.c.o' failed
     [exec] CMakeFiles/Makefile2:1005: recipe for target 
'runtime/alloc/CMakeFiles/alloc.dir/all' failed
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:26:7:
 error: no previous prototype for function 'fromspace_ptr' 
[-Werror,-Wmissing-prototypes]
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/collect.c:34char
 *fromspace_ptr() {:
     [exec] 6:      ^ 
     [exec] error: no previous prototype for function 'during_gc' 
[-Werror,-Wmissing-prototypes]
     [exec] bool during_gc() {
     [exec]      ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:30:7:
 error: no previous prototype for function 'oldspace_ptr' 
[-Werror,-Wmissing-prototypes]
     [exec] char *oldspace_ptr() {
     [exec]       ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:34:8:
 error: no previous prototype for function 'alloc_ptr' 
[-Werror,-Wmissing-prototypes]
     [exec] char **alloc_ptr() {
     [exec]        ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:38:8:
 error: no previous prototype for function 'old_alloc_ptr' 
[-Werror,-Wmissing-prototypes]
     [exec] char **old_alloc_ptr() {
     [exec]        ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:42:6:
 error: no previous prototype for function 'fromspace_id' 
[-Werror,-Wmissing-prototypes]
     [exec] char fromspace_id() {
     [exec]      ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:62:37:
 error: cast from 'char *' to 'memory_block_header *' increases required 
alignment from 1 to 8 [-Werror,-Wcast-align]
     [exec]   memory_block_header *superblock = (memory_block_header 
*)(fromspace.semispace_id == 0 ? fromspace.first_block : first_tospace_block);
     [exec]                                     
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:64:44:
 error: cast from 'char *' to 'memory_block_header *' increases required 
alignment from 1 to 8 [-Werror,-Wcast-align]
     [exec]     memory_block_header* next_superblock = (memory_block_header 
*)superblock->next_superblock;
     [exec]                                            
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:61:6:
 error: no previous prototype for function 'freeAllKoreMem' 
[-Werror,-Wmissing-prototypes]
     [exec] void freeAllKoreMem() {
     [exec]      ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/collect.c:125:23:
 error: cast from 'char *' to 'char **' increases required alignment from 1 
to 8 [-Werror,-Wcast-align]
     [exec]   char *next_block = *(char **)current_tospace_start;
     [exec]                       ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/collect.c:135:22:
 error: cast from 'char *' to 'block *' (aka 'struct block *') increases 
required alignment from 1 to 8 [-Werror,-Wcast-align]
     [exec]   block *currBlock = (block *)scan_ptr;
     [exec]                      ^~~~~~~~~~~~~~~~~
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/collect.c:194:6:
 error: no previous prototype for function 'koreCollect' 
[-Werror,-Wmissing-prototypes]
     [exec] void koreCollect(block** root) {
     [exec]      ^
     [exec] 4 errors generated.
     [exec] make[2]: *** [runtime/alloc/CMakeFiles/alloc.dir/collect.c.o] 
Error 1
     [exec] make[2]: *** Waiting for unfinished jobs....
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:90:18:
 error: arithmetic on a pointer to void is a GNU extension 
[-Werror,-Wpointer-arith]
     [exec]   superblock_ptr += BLOCK_SIZE;
     [exec]   ~~~~~~~~~~~~~~ ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:99:41:
 error: cast from 'char *' to 'memory_block_header *' increases required 
alignment from 1 to 8 [-Werror,-Wcast-align]
     [exec]       memory_block_header *nextHeader = (memory_block_header 
*)nextBlock;
     [exec]                                         
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:103:20:
 error: cast from 'char *' to 'char **' increases required alignment from 1 
to 8 [-Werror,-Wcast-align]
     [exec]       nextBlock = *(char**)space->block_start;
     [exec]                    ^~~~~~~~~~~~~~~~~~~~~~~~~~
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:106:12:
 error: cast from 'char *' to 'uint64_t *' (aka 'unsigned long *') increases 
required alignment from 1 to 8 [-Werror,-Wcast-align]
     [exec]           *(uint64_t *)space->block = NOT_YOUNG_OBJECT_BIT; // 8 
bit sentinel value
     [exec]            ^~~~~~~~~~~~~~~~~~~~~~~~
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:108:12:
 error: cast from 'char *' to 'uint64_t *' (aka 'unsigned long *') increases 
required alignment from 1 to 8 [-Werror,-Wcast-align]
     [exec]           *(uint64_t *)space->block = space->block_end - 
space->block - 8; // 16-bit or more sentinel value
     [exec]            ^~~~~~~~~~~~~~~~~~~~~~~~
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:114:10:
 error: cast from 'char *' to 'char **' increases required alignment from 1 
to 8 [-Werror,-Wcast-align]
     [exec]         *(char **)space->block_start = nextBlock;
     [exec]          ^~~~~~~~~~~~~~~~~~~~~~~~~~~
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c:115:43:
 error: cast from 'char *' to 'memory_block_header *' increases required 
alignment from 1 to 8 [-Werror,-Wcast-align]
     [exec]         memory_block_header *nextHeader = (memory_block_header 
*)nextBlock;
     [exec]                                           
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     [exec] 15 errors generated.
     [exec] make[2]: *** [runtime/alloc/CMakeFiles/alloc.dir/alloc.c.o] Error 
1
     [exec] make[1]: *** [runtime/alloc/CMakeFiles/alloc.dir/all] Error 2
     [exec] In file included from 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/strings/bytes.cpp:9:
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/include/runtime/header.h:38:15:
 error: flexible array members are a C99 feature [-Werror,-Wc99-extensions]
     [exec]     uint64_t *children[];
     [exec]               ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/include/runtime/header.h:45:10:
 error: flexible array members are a C99 feature [-Werror,-Wc99-extensions]
     [exec]     char data[];
     [exec]          ^
     [exec] runtime/strings/CMakeFiles/strings.dir/build.make:86: recipe for 
target 'runtime/strings/CMakeFiles/strings.dir/bytes.cpp.o' failed
     [exec] 2 errors generated.
     [exec] make[2]: *** [runtime/strings/CMakeFiles/strings.dir/bytes.cpp.o] 
Error 1
     [exec] make[2]: *** Waiting for unfinished jobs....
     [exec] [ 36%] Linking CXX static library libarithmetic.a
     [exec] [ 36%] Linking CXX static library libHello.a
     [exec] [ 36%] Built target arithmetic
     [exec] [ 36%] Built target Hello
     [exec] In file included from 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/strings/strings.cpp:15:
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/include/runtime/header.h:38:15:
 error: flexible array members are a C99 feature [-Werror,-Wc99-extensions]
     [exec]     uint64_t *children[];
     [exec]               ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/include/runtime/header.h:45:10:
 error: flexible array members are a C99 feature [-Werror,-Wc99-extensions]
     [exec]     char data[];
     [exec]          ^
     [exec] 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/runtime/strings/strings.cpp:206:19:
 error: variable length arrays are a C99 feature [-Werror,-Wvla-extension]
     [exec]     size_t matches[len(haystack)];
     [exec]                   ^
     [exec] 3 errors generated.
     [exec] make[2]: *** 
[runtime/strings/CMakeFiles/strings.dir/strings.cpp.o] Error 1
     [exec] make[1]: *** [runtime/strings/CMakeFiles/strings.dir/all] Error 2
     [exec] runtime/strings/CMakeFiles/strings.dir/build.make:62: recipe for 
target 'runtime/strings/CMakeFiles/strings.dir/strings.cpp.o' failed
     [exec] CMakeFiles/Makefile2:950: recipe for target 
'runtime/strings/CMakeFiles/strings.dir/all' failed
     [exec] [ 40%] Linking CXX static library libParser.a
     [exec] [ 40%] Linking CXX static library libAST.a
     [exec] [ 40%] Built target AST
     [exec] [ 40%] Built target Parser
     [exec] kore-0.0.1.0: unregistering (switching from 
/opt/k/k/llvm-backend/src/main/native/llvm-backend/matching/submodules/kore/src/main/haskell/kore/
 to 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/matching/submodules/kore/src/main/haskell/kore/)
     [exec] matching-0.1.0.0: unregistering (missing dependencies: kore)
     [exec] kore-0.0.1.0: configure (lib + exe)
     [exec] kore-0.0.1.0: build (lib + exe)
     [exec] 
     [exec] --  While building package kore-0.0.1.0 using:
     [exec]       
/home/christos/.stack/setup-exe-cache/x86_64-linux/Cabal-simple_mPHDZzAJ_2.2.0.1_ghc-8.4.4
 --builddir=.stack-work/dist/x86_64-linux/Cabal-2.2.0.1 build lib:kore 
exe:kore-exec exe:kore-format 
exe:kore-paCMakeFiles/matching.dir/build.make:65: recipe for target 
'bin/llvm-kompile-matching' failed
     [exec] CMakeFiles/Makefile2:67: recipe for target 
'CMakeFiles/matching.dir/all' failed
     [exec] Makefile:129: recipe for target 'all' failed
     [exec] rser exe:prover --ghc-options " -ddump-hi -ddump-to-file"
     [exec]     Process exited with code: ExitFailure 1
     [exec]     Logs have been written to: 
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/matching/.stack-work/logs/kore-0.0.1.0.log
     [exec] 
     [exec]     Configuring kore-0.0.1.0...
     [exec]     Preprocessing library for kore-0.0.1.0..
     [exec]     Building library for kore-0.0.1.0..
     [exec]     [102 of 159] Compiling Kore.SMT.SMT     ( 
src/Kore/SMT/SMT.hs, 
.stack-work/dist/x86_64-linux/Cabal-2.2.0.1/build/Kore/SMT/SMT.o ) [Data.SBV 
changed]
     [exec]     
     [exec]     
/opt/k/uiuc/k/llvm-backend/src/main/native/llvm-backend/matching/submodules/kore/src/main/haskell/kore/src/Kore/SMT/SMT.hs:47:1:
 error:
     [exec]         Could not find module ‘Data.SBV’
     [exec]         There are files missing in the ‘sbv-7.10’ package,
     [exec]         try running 'ghc-pkg check'.
     [exec]         Use -v to see a list of the files searched for.
     [exec]        |
     [exec]     47 | import Data.SBV
     [exec]        | ^^^^^^^^^^^^^^^
     [exec] make[2]: *** [bin/llvm-kompile-matching] Error 1
     [exec] make[1]: *** [CMakeFiles/matching.dir/all] Error 2
     [exec] make: *** [all] Error 2
[INFO] 
------------------------------------------------------------------------
[INFO] Reactor Summary:
[INFO] 
[INFO] K Framework Tool Parent ............................ 
SUCCESS [  1.492 s]
[INFO] K Framework KORE ................................... 
SUCCESS [ 47.186 s]
[INFO] K Framework Tool Kernel ............................ 
SUCCESS [ 48.106 s]
[INFO] K Framework KTree .................................. 
SUCCESS [  0.572 s]
[INFO] K Framework Ocaml Backend .......................... 
SUCCESS [  1.331 s]
[INFO] K Framework Java Backend ........................... 
SUCCESS [  8.360 s]
[INFO] K Framework Haskell Backend ........................ 
SUCCESS [  0.324 s]
[INFO] K Framework LLVM Backend ........................... 
FAILURE [ 56.346 s]
[INFO] K Framework Tool Distribution ...................... 
SKIPPED
[INFO] 
------------------------------------------------------------------------
[INFO] BUILD FAILURE
[INFO] 
------------------------------------------------------------------------
[INFO] Total time: 02:44 min
[INFO] Finished at: 2019-01-23T16:49:12Z
[INFO] Final Memory: 42M/147M
[INFO] 
------------------------------------------------------------------------
[ERROR] Failed to execute goal 
org.apache.maven.plugins:maven-antrun-plugin:1.7:run 
(build-llvm) on project llvm-backend: An Ant 
BuildException has occured: exec returned: 2
[ERROR] around Ant part ...<exec failonerror="true" 
dir="/opt/k/uiuc/k/llvm-backend/target/build" executable="make">... @ 11:92 
in /opt/k/uiuc/k/llvm-backend/target/antrun/build-main.xml
[ERROR] -> [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
[ERROR] 
[ERROR] After correcting the problems, you can resume the build 
with the command
[ERROR]   mvn <goals> -rf :llvm-backend