k: [Bug] [mvn package|kompile] - Issues while installing, building and running K on Apple Silicon

K Version: v5.1.226-1-g40c4932f6-dirty

Description

Issues have been found while trying to install the k framework via package, to build with maven and to use the kompile command on Apple Silicon machines (M1 chips).

- INSTALLATION VIA BREW PACKAGE:

After installing K using the package available at the release page, an attempt to use the kompile command to build the definitions for the first K program presented in K training lesson 2 returns the following message:

dyld: Library not loaded: /opt/homebrew/opt/jemalloc/lib/libjemalloc.2.dylib
 Referenced from: /opt/homebrew/lib/kframework/../../bin/llvm-kompile-codegen
 Reason: no suitable image found. Did find:
    /opt/homebrew/opt/jemalloc/lib/libjemalloc.2.dylib: mach-o, but wrong architecture
    /opt/homebrew/Cellar/jemalloc/5.2.1_1/lib/libjemalloc.2.dylib: mach-o, but wrong architecture
/opt/homebrew/lib/kframework/../../bin/llvm-kompile: line 44: 9377 Abort trap: 6     "$(dirname "$0")"/llvm-kompile-codegen "$definition" "$dt_dir"/dt.yaml "$dt_dir" $debug > "$mod"
[Error] Critical: llvm-kompile returned nonzero exit code: 134
Examine output to see errors.

Jemalloc supports Apple Silicon, which leads me to believe that it must be something related to how the K release package has been built.

- BUILDING WITH MAVEN:

When building with maven, errors were be triggered in the stage “K Framework LLVM Backend”. The errors are related to the llvm 13, which, from my understanding, is not supported to build the K framework. To solve this issue, an earlier version of llvm must be installed. I’ve solved this using brew’s llvm@12 package.

After doing so, I still could not successfully build the project as many of the libraries which have been installed as dependencies could not be found. The error messages are as follows:

This issue seems to be related to the change in brew’s default installation directory, as packages are now being installed in the /opt/homebrew/ subfolders. A workaround to this problem is to create a symbolic link from the /opt/homebrew/lib, /opt/homebrew/include, and /opt/homebrew/bin to the /usr/local/ folder. This can be done using the following commands:

cd /usr/local/
sudo ln -s /opt/homebrew/lib lib
sudo ln -s /opt/homebrew/include include
sudo ln -s /opt/homebrew/bin bin

After adding the symbolic links, the libraries could be found during the building process. Still, the following error would be triggered in the llvm backend building stage:

[exec] /Users/acassimiro/Documents/tools/k/llvm-backend/src/main/native/llvm-backend/runtime/meta/ffi.cpp:241:11: error: enumeration value ‘FFI_BAD_ARGTYPE’ not handled in switch [-Werror,-Wswitch]

Which was fixed after adding case FFI_BAD_ARGTYPE: throw std::invalid_argument(“Bad argument type”); break; to the k/llvm-backend/src/main/native/llvm-backend/runtime/meta/ffi.cpp file on line 247.

With this, I’ve managed to successfully build K using mvn package -DskipTests, but I still cannot execute the kompile command.

- EXECUTING KOMPILE WITH THE BINARIES GENERATED AFTER COMPILING FROM THE SOURCE:

Finally, after building K, the following error is shown after trying to call compile on a simple K file:

ld: warning: ignoring file tmp.bN8Tml3rEu/equality.ll.o, building for macOS-arm64 but attempting to link with file built for unknown-x86_64ld: warning: ignoring file tmp.bN8Tml3rEu/asm.o, building for macOS-arm64 but attempting to link with file built for unknown-x86_64

ld: warning: ignoring file tmp.bN8Tml3rEu/finish_rewriting.ll.o, building for macOS-arm64 but attempting to link with file built for unknown-x86_64
ld: warning: ignoring file tmp.bN8Tml3rEu/fresh.ll.o, building for macOS-arm64 but attempting to link with file built for unknown-x86_64
ld: warning: ignoring file tmp.bN8Tml3rEu/move_int.ll.o, building for macOS-arm64 but attempting to link with file built for unknown-x86_64
ld: warning: ignoring file tmp.bN8Tml3rEu/getTag.ll.o, building for macOS-arm64 but attempting to link with file built for unknown-x86_64
ld: warning: ignoring file tmp.bN8Tml3rEu/string_equal.ll.o, building for macOS-arm64 but attempting to link with file built for unknown-x86_64
ld: warning: ignoring file tmp.bN8Tml3rEu/take_steps.ll.o, building for macOS-arm64 but attempting to link with file built for unknown-x86_64
ld: warning: ignoring file tmp.bN8Tml3rEu/move_float.ll.o, building for macOS-arm64 but attempting to link with file built for unknown-x86_64
Undefined symbols for architecture arm64:
  "_evaluateFunctionSymbol", referenced from:
      _parseConfiguration in libutil.a(ConfigurationParser.cpp.o)
      substituteInternal(block*) in libmeta.a(substitution.cpp.o)
  "_finish_rewriting", referenced from:
      _main in main-1610ae.o
  "_first_inj_tag", referenced from:
      _parseConfiguration in libutil.a(ConfigurationParser.cpp.o)
  "_getBlockHeaderForSymbol", referenced from:
      _parseConfiguration in libutil.a(ConfigurationParser.cpp.o)
  "_getInjectionForSortOfTag", referenced from:
      substituteInternal(block*) in libmeta.a(substitution.cpp.o)
  "_getLayoutData", referenced from:
      _koreCollect in libcollect.a(collect.cpp.o)
      _parseConfiguration in libutil.a(ConfigurationParser.cpp.o)
      debruijnizeInternal(block*) in libmeta.a(substitution.cpp.o)
      replaceBinderInternal(block*) in libmeta.a(substitution.cpp.o)
      substituteInternal(block*) in libmeta.a(substitution.cpp.o)
      _incrementDebruijn in libmeta.a(substitution.cpp.o)
      _debruijnize in libmeta.a(substitution.cpp.o)
      ...
  "_getSymbolNameForTag", referenced from:
      _printConfigurationInternal in libutil.a(ConfigurationPrinter.cpp.o)
  "_getTagForSymbolNameInternal", referenced from:
      _getTagForSymbolName in libutil.a(ConfigurationParser.cpp.o)
  "_getToken", referenced from:
      _parseConfiguration in libutil.a(ConfigurationParser.cpp.o)
  "_get_gc_threshold", referenced from:
      _is_collection in libcollect.a(collect.cpp.o)
  "_hook_KEQUAL_eq", referenced from:
      substituteInternal(block*) in libmeta.a(substitution.cpp.o)
      _hook_LIST_in in libcollections.a(lists.cpp.o)
      immer::detail::rbts::rrbtree<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u>::equals(immer::detail::rbts::rrbtree<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> const&) const in libcollections.a(lists.cpp.o)
      bool immer::detail::rbts::equals_visitor::visit_leaf<immer::detail::rbts::leaf_sub_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::leaf_sub_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::rrbtree_iterator<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u>&>(immer::detail::rbts::leaf_sub_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::leaf_sub_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::rrbtree_iterator<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u>&, unsigned long) in libcollections.a(lists.cpp.o)
      bool immer::detail::rbts::equals_visitor::visit_leaf<immer::detail::rbts::leaf_sub_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::relaxed_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::rrbtree_iterator<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u>&>(immer::detail::rbts::leaf_sub_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::relaxed_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::rrbtree_iterator<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u>&, unsigned long) in libcollections.a(lists.cpp.o)
      bool immer::detail::rbts::equals_visitor::visit_leaf<immer::detail::rbts::full_leaf_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::leaf_sub_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::rrbtree_iterator<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u>&>(immer::detail::rbts::full_leaf_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::leaf_sub_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::rrbtree_iterator<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u>&, unsigned long) in libcollections.a(lists.cpp.o)
      bool immer::detail::rbts::equals_visitor::visit_leaf<immer::detail::rbts::full_leaf_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::relaxed_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::rrbtree_iterator<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u>&>(immer::detail::rbts::full_leaf_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::relaxed_pos<immer::detail::rbts::node<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u> >&, immer::detail::rbts::rrbtree_iterator<KElem, immer::memory_policy<immer::heap_policy<kore_alloc_heap>, immer::no_refcount_policy, immer::gc_transience_policy, false, false>, 5u, 5u>&, unsigned long) in libcollections.a(lists.cpp.o)
      ...
  "_isSymbolABinder", referenced from:
      _parseConfiguration in libutil.a(ConfigurationParser.cpp.o)
      debruijnizeInternal(block*) in libmeta.a(substitution.cpp.o)
      replaceBinderInternal(block*) in libmeta.a(substitution.cpp.o)
      substituteInternal(block*) in libmeta.a(substitution.cpp.o)
      _incrementDebruijn in libmeta.a(substitution.cpp.o)
      _printConfigurationInternal in libutil.a(ConfigurationPrinter.cpp.o)
  "_isSymbolAFunction", referenced from:
      _parseConfiguration in libutil.a(ConfigurationParser.cpp.o)
      substituteInternal(block*) in libmeta.a(substitution.cpp.o)
  "_last_inj_tag", referenced from:
      _parseConfiguration in libutil.a(ConfigurationParser.cpp.o)
  "_move_float", referenced from:
      _hook_STRING_string2float in libstrings.a(strings.cpp.o)
      _hook_FLOAT_ceil in libarithmetic.a(float.cpp.o)
      _hook_FLOAT_floor in libarithmetic.a(float.cpp.o)
      _hook_FLOAT_trunc in libarithmetic.a(float.cpp.o)
      _hook_FLOAT_round in libarithmetic.a(float.cpp.o)
      _hook_FLOAT_int2float in libarithmetic.a(float.cpp.o)
      _hook_FLOAT_sin in libarithmetic.a(float.cpp.o)
      ...
  "_move_int", referenced from:
      _hook_STRING_ord in libstrings.a(strings.cpp.o)
      _hook_STRING_find in libstrings.a(strings.cpp.o)
      _hook_STRING_rfind in libstrings.a(strings.cpp.o)
      _hook_STRING_findChar in libstrings.a(strings.cpp.o)
      _hook_STRING_rfindChar in libstrings.a(strings.cpp.o)
      _hook_STRING_string2base_long in libstrings.a(strings.cpp.o)
      _hook_STRING_countAllOccurrences in libstrings.a(strings.cpp.o)
      ...
  "_output_file", referenced from:
      _main in main-1610ae.o
  "_set_gc_threshold", referenced from:
      _koreCollect in libcollect.a(collect.cpp.o)
  "_sort_table", referenced from:
     -u command line option
  "_statistics", referenced from:
      _main in main-1610ae.o
  "_storeSymbolChildren", referenced from:
      _parseConfiguration in libutil.a(ConfigurationParser.cpp.o)
  "_take_steps", referenced from:
      _main in main-1610ae.o
  "_visitChildren", referenced from:
      _printConfigurationInternal in libutil.a(ConfigurationPrinter.cpp.o)
ld: symbol(s) not found for architecture arm64
clang-12: error: linker command failed with exit code 1 (use -v to see invocation)
[Error] Critical: llvm-kompile returned nonzero exit code: 1
Examine output to see errors.
[Warning] Compiler: Could not find main syntax module with name
LESSON-02-A-SYNTAX in definition.  Use --syntax-module to specify one. Using
LESSON-02-A as default.

I’m still looking for a workaround for this lasts issue.

Input Files

The input file used was the first K example provided in the K-tutorial second lesson.

Reproduction Steps

Installation via brew package was done following the instructions provided in the K-framework release page.

Building with maven was done with mvn package -DskipTests.

The kompilation attempt was done with kompile lesson-02-a.k.

Expected Behavior

With the instructions available in the release page and the git’s README information, I expected to be able to successfully install the K-framework with no issues in its functionalities.