• Stars
    star
    447
  • Rank 97,700 (Top 2 %)
  • Language
    Java
  • License
    BSD 3-Clause "New...
  • Created almost 9 years ago
  • Updated about 1 month ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

K Framework Tools 7.0
copyright permalink
Copyright (c) K Team. All Rights Reserved.
README.html

Join the chat on Matrix

Introduction

The K Framework is a tool for designing and modeling programming languages and software/hardware systems. At the core of the K Framework is a programming, modeling, and specification language called K. The K Framework includes tools for compiling K specifications to build interpreters, model checkers, verifiers, associated documentation, and more.

Quick Start

If you are not a K developer, but just want to get started using K, we provide a streamlined installation process for any system that supports Nix:

bash <(curl https://kframework.org/install)
kup install k

For more information on the kup tool and other packaged releases of K, please refer to our installation notes.

Preface

This is a readme file for K developers. Users should feel comfortable using the command line, as we do not provide GUI tools at this time.

K-based tool users should:

  1. Consult their tool documentation for build/installation instructions.
  2. If needed, download a packaged release of the K Framework as part of their tool setup process.

If you are interested in quickly trying out the K Framework without building from source, please see our packaged release installation guide.

The rest of this file assumes you intend to build and install the K Framework from source.

Note that the K Framework can only be built on (x86-64) Linux-like systems, e.g., this also includes macOS/brew (x86-64) as well as the Windows Subsystem for Linux. All 32-bit systems are not supported. See the installation notes for details about supported configurations and system setup.

Contents

  1. Prerequisite Install Guide
  2. Build and Install Guide
  3. IDE Setup
  4. Running the Test Suite
  5. Changing the KORE Data Structures
  6. Building the Final Release Directory/Archives
  7. Compiling Definitions and Running Programs
  8. Installing Python Support
  9. Troubleshooting

Prerequisite Install Guide

Before building and installing the K Framework, the following prerequisites must first be installed.

The Short Version

On Ubuntu Linux 22.04 (Jammy):

git submodule update --init --recursive
sudo apt-get install build-essential m4 openjdk-11-jdk libfmt-dev libgmp-dev libmpfr-dev pkg-config flex bison z3 libz3-dev maven python3 python3-dev cmake gcc g++ clang-14 lld-14 llvm-14-tools zlib1g-dev libboost-test-dev libyaml-dev libjemalloc-dev
curl -sSL https://get.haskellstack.org/ | sh

On Ubuntu Linux 20.04 (Focal):

Note: the installation process is very similar to the above, the only difference is that clang, lld and llvm-tools have to be version 12.

git submodule update --init --recursive
sudo apt-get install build-essential m4 openjdk-11-jdk libfmt-dev libgmp-dev libmpfr-dev pkg-config flex bison z3 libz3-dev maven python3 python3-dev cmake gcc g++ clang-12 lld-12 llvm-12-tools zlib1g-dev libboost-test-dev libyaml-dev libjemalloc-dev
curl -sSL https://get.haskellstack.org/ | sh

On Arch Linux:

git submodule update --init --recursive
sudo pacman -S git maven jdk-openjdk cmake boost fmt libyaml jemalloc clang llvm lld zlib gmp mpfr z3 curl stack base-devel base python

If you install this list of dependencies, continue directly to the Build and Install Guide.

On macOS using Homebrew:

git submodule update --init --recursive
brew install bison boost cmake flex fmt gcc gmp openjdk jemalloc libyaml llvm@15 make maven mpfr pkg-config python stack zlib z3

Note: in this case llvm@15 is required.

The Long Version

The following dependencies are needed either at build time or runtime:

  • bison
  • boost
  • cmake
  • flex
  • fmt
  • gcc
  • gmp
  • jdk (version 11 or greater)
  • libjemalloc
  • libyaml
  • llvm (We require version 10 or greater for clang, lld, and llvm-tools. On some distributions, the utilities below are also needed and packaged separately.)
  • make
  • maven
  • mpfr
  • pkg-config
  • python
  • stack
  • zlib
  • z3 (on some distributions libz3 is also needed and packaged separately) Note that you need version 4.8.15 of Z3, which may require you to build and install from source if your package manager does not supply it. Other versions are known to have bugs and performance regressions likely to cause issues in the K test suite.

Typically, these can all be installed from your package manager. On some system configurations, special installation steps or post-installation configuration steps are required. See the notes below.

Installation Notes

  1. Java Development Kit (required JDK11 or higher)

    • Linux: Download from package manager (e.g. sudo apt-get install openjdk-11-jdk).

    • macOS/brew: Download from package manager (e.g. brew install java).

    To make sure that everything works you should be able to call java -version and javac -version from a terminal.

  2. LLVM

    • macOS/brew: Since LLVM is distributed as a keg-only package, we must explicitly make it available for command line usage. See the results of the brew info llvm command for more information on how to do this. Additionally, the default version of LLVM supplied by Homebrew is newer than the version supported by K. The formula llvm@15 should be used instead of llvm.
  3. Flex / Bison

    • macOS/brew: The versions of these packages supplied by the OS are too old, and are not compatible with the K build. You must ensure that the Homebrew-installed versions are first on your PATH when building K (i.e. which flex is not /usr/bin/flex).
  4. Apache Maven

    • Linux: Download from package manager (e.g. sudo apt-get install maven).

    • macOS/brew: Download it from a package manager or from http://maven.apache.org/download.cgi and follow the instructions on the webpage.

    Maven usually requires setting an environment variable JAVA_HOME pointing to the installation directory of the JDK (not to be mistaken with JRE).

    You can test if it works by calling mvn -version in a terminal. This will provide the information about the JDK Maven is using, in case it is the wrong one.

  5. Haskell Stack

    To install, go to https://docs.haskellstack.org/en/stable/README/ and follow the instructions. You may need to do stack upgrade to ensure the latest version of Haskell Stack.

Build and Install Guide

Building with Maven

Checkout the project source at your desired location and call mvn package from the main directory to build the distribution. For convenient usage, you can update your $PATH with <checkout-dir>/k-distribution/target/release/k/bin (strongly recommended, but optional).

You are also encouraged to set the environment variable MAVEN_OPTS to -XX:+TieredCompilation, which will significantly speed up the incremental build process.

Apple Silicon Support

K currently offers partial support for Apple Silicon; the toolchain has been tested and works on ARM macOS, but is not yet part of our CI/CI pipeline. To build K on an Apple Silicon machine, ensure the following steps are followed in addition to the usual Maven build setup:

  • Ensure that Homebrew-installed versions of llvm-config, flex and bison are on your PATH ahead of any macOS-supplied versions.
    • direnv offers a convenient way to automate this. To do so:
      brew install direnv
      # Follow the instructions at https://direnv.net/docs/hook.html
      # ...for example, if your shell is bash, run:
      #   echo 'eval "$(direnv hook bash)"' >> ~/.bashrc
      # then restart your shell.
      cp macos-envrc .envrc
      direnv allow
      # You should see a message like:
      #   direnv: loading .../k/.envrc
      #   direnv: export ~PATH
      # The llvm-config binary should also be on your PATH; check with:
      which llvm-config
  • Pass -Dstack.extra-opts='--compiler ghc-8.10.7 --system-ghc' as an additional argument to mvn package when building the toolchain.
    • This is a workaround for stack and ghc not yet properly supporting ARM macOS; the underlying problem is likely to be fixed at some point in the future.
    • See the documentation and associated PR for more details.

Building with Nix flakes (Recommended)

We now support building K using nix flakes. To set up nix flakes you will need to be on nix 2.4 or higher and follow the instructions here.

For example, if you are on a standard Linux distribution, such as Ubuntu, first install nix and then enable flakes by editing either ~/.config/nix/nix.conf or /etc/nix/nix.conf and adding:

experimental-features = nix-command flakes

This is needed to expose the Nix 2.0 CLI and flakes support that are hidden behind feature-flags.

By default, Nix will build the project and its transitive dependencies from source, which can take up to an hour. We recommend setting up the binary cache to speed up the build process significantly. You will also need to add the following sections to /etc/nix/nix.conf or, if you are a trusted user, ~/.config/nix/nix.conf (if you don't know what a "trusted user" is, you probably want to do the former):

trusted-public-keys = ... hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
substituters = ... https://cache.iog.io

i.e. if the file was originally

substituters = https://cache.nixos.org
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=

it will now read

substituters = https://cache.nixos.org https://cache.iog.io
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=

To build the K Framework itself, run:

nix build .

This will build all of K and put a link to the resulting binaries in the result/ folder.

Note: Mac users, especially those running M1/M2 Macs may find nix segfaulting on occasion. If this happens, try running the nix command like this: GC_DONT_GC=1 nix build .

If you want to temporarily add the K binaries (such as kompile or kast) to the current shell, run

nix shell .

To run the integration tests:

nix build .#test

If you change any pom.xml, you must run

nix run .#update-maven

and commit the updated nix/mavenix.lock file.

Building with Nix (not recommended, use Nix flakes)

To build the K Framework itself, run:

nix-build -A k

The various backends are provided as separate packages:

nix-build -A llvm-backend
nix-build -A haskell-backend

To run the integration tests:

nix-build test.nix

You can enter a development environment for working on the K Framework frontend by running:

nix-shell

To create a development environment for a project that depends on the K Framework, you can add a shell.nix based on this template:

# shell.nix
let
  kframework = import ./path/to/k {};
  inherit (kframework) mkShell;
in
mkShell {
  buildInputs = [
    kframework.k
    clang kframework.llvm-backend
    kframework.haskell-backend
  ];
}

If you change any pom.xml, you must run ./nix/update-maven.sh.

IDE Setup

General

You should run K from the k-distribution project, because it is the only project to have the complete classpath and therefore all backends.

Eclipse

N.B. the Eclipse internal compiler may generate false compilation errors (there are bugs in its support of Scala mixed compilation). We recommend using IntelliJ IDEA if at all possible.

To autogenerate an Eclipse project for K, run mvn install -DskipKTest; mvn eclipse:eclipse on the command line, and then go into each of the kore and tiny directories and run sbt eclipse. Then start eclipse and go to File->Import->General->Existing projects into workspace, and select the directory of the installation. You should only add the leaves to the workspace, because eclipse does not support hierarchical projects.

IntelliJ IDEA

IntelliJ IDEA comes with built-in maven integration. For more information, refer to the IntelliJ IDEA wiki

Running the Test Suite

To completely test the current version of the K framework, run mvn verify. This normally takes roughly 30 minutes on a fast machine. If you are interested only in running the unit tests and checkstyle goals, run mvn verify -DskipKTest to skip the lengthy ktest execution.

Changing the KORE Data Structures

If you need to change the KORE data structures (unless you are a K core developer, you probably do not), see Guide-for-changing-the-KORE-data-structures.

Building the Final Release Directory/Archives

Call mvn install in the base directory. This will attach an artifact to the local maven repository containing a zip and tar.gz of the distribution.

The functionality to create a tagged release is currently incomplete.

Compiling Definitions and Running Programs

Assuming k-distribution/target/release/k/bin is in your path, you can compile definitions using the kompile command. To execute a program you can use krun.

For running either program in the debugger, use the main class org.kframework.main.Main with an additional argument -kompile or -krun added before other command line arguments, and use the classpath from the k-distribution module.

Installing Python Support

Python tools for K can be found under runtimeverification/pyk.

Troubleshooting

Common build-time error messages:

  • Error: JAVA_HOME not found in your environment. Please set the JAVA_HOME variable in your environment to match the location of your Java installation.

    • Make sure JAVA_HOME points to the JDK and not the JRE directory.
  • [WARNING] Cannot get the branch information from the git repository: Detecting the current branch failed: 'git' is not recognized as an internal or external command, operable program or batch file.

    • git might not be installed on your system. Make sure that you can execute git from the command line.
  • 1) Error injecting constructor, java.lang.Error: Unresolved compilation problems: The import org.kframework.parser.outer.Outer cannot be resolved Outer cannot be resolved

    • You may run into this issue if target/generated-sources/javacc is not added to the build path of your IDE. Generally this is solved by regenerating your project / re-syncing it with the pom.xml.
  • [ERROR] Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.1:compile (default-compile) on project k-core: Fatal error compiling: invalid target release: 11 -> [Help 1]

    • You either do not have Java 11 installed, or $JAVA_HOME does not point to a Java 11 JDK.
  • [ERROR] Failed to execute goal org.apache.maven.plugins:maven-antrun-plugin:1.7:run (build-haskell) on project haskell-backend: An Ant BuildException has occured: exec returned: 1

    and scrolling up, you see an error message similar to:

    [exec] Installing GHC ... [exec] ghc-pkg: Couldn't open database $HOME/.stack/programs/x86_64-linux/ghc-tinfo6-8.10.1/lib/ghc-8.10.1/package.conf.d for modification: {handle: $HOME/.stack/programs/x86_64-linux/ghc-tinfo6-8.10.1/lib/ghc-8.10.1/package.conf.d/package.cache.lock}: hLock: invalid argument (Invalid argument)

    • If you are using a WSL version 1 environment, then you have encountered a known issue with the latest versions of GHC. In this case, please either:
      • upgrade to WSL version 2,
      • install a packaged release for your WSL version 1 distribution,
      • switch to a supported system configuration (e.g. Linux on a virtual machine), or
      • if you do not need the symbolic execution capabilities of the K Framework, disable them at build time (and remove the GHC dependency) by doing: mvn package -Dhaskell.backend.skip.

If something unexpected happens and the project fails to build, try mvn clean and rebuild the entire project. Generally speaking, however, the project should build incrementally without needing to be cleaned first.

If you are doing work with snapshot dependencies, you can update them to the latest version by running maven with the -U flag.

If you are configuring artifacts in a repository and need to purge the local repository's cache of artifacts, you can run mvn dependency:purge-local-repository.

If tests fail but you want to run the build anyway to see what happens, you can use mvn package -DskipTests.

If you still cannot build, please contact a K developer.

More Repositories

1

verified-smart-contracts

Smart contracts which are formally verified
Solidity
717
star
2

evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)
Python
507
star
3

haskell-backend

The symbolic execution engine powering the K Framework
Haskell
210
star
4

iele-semantics

Semantics of Virtual Machine for IELE prototype blockchain
HTML
130
star
5

publications

Publications of Runtime Verification, Inc.
HTML
87
star
6

wasm-semantics

A Prototype Formal Semantics of WebAssembly in K
WebAssembly
78
star
7

kontrol

Python
49
star
8

erc20-semantics

ERC20 in K
47
star
9

javamop

Runtime verification system for Java, using AspectJ for instrumentation.
Java
44
star
10

llvm-backend

KORE to llvm translation
C++
31
star
11

deposit-contract-verification

Makefile
30
star
12

plutus-core-semantics

Haskell
27
star
13

algorand-verification

Formal verification of the Algorand consensus protocol
Coq
26
star
14

beacon-chain-spec

Formalization of the Beacon Chain Phase 0 Specification in K
TeX
20
star
15

python-semantics

The semantics of Python in K
Python
19
star
16

beacon-chain-verification

TeX
18
star
17

michelson-semantics

A K semantics of Tezos' Michelson language.
Makefile
17
star
18

casper-proofs

Coq definitions and lemmas for verification of Casper
TeX
17
star
19

solidity

Fork of the Solidity Compiler for compiling Solidity to IELE
C++
16
star
20

rv-monitor

RV-Monitor core system code
Java
15
star
21

avm-semantics

Python
15
star
22

pyk

Python tools for the K Framework
Python
13
star
23

foundry-upgradeable-contracts-examples

Example tests for exploring upgradeable contracts with Foundry
Solidity
13
star
24

kontrol-demo

Foundry blog posts' executable demos
Solidity
12
star
25

zero-to-k-tutorial

Makefile
12
star
26

simbolik-vscode

TypeScript
12
star
27

k-editor-support

Plugin files for editing K files
Java
11
star
28

erc777-semantics

Makefile
11
star
29

mpfr-java

GNU MPFR Java Bindings
Java
10
star
30

kontrol-solady

Solady formal verification with Kontrol
Solidity
10
star
31

polkadot-verification

Verification of Polkadot WASM code
WebAssembly
9
star
32

secureum-kontrol

Solidity
9
star
33

kontrol-cheatcodes

Cheatcodes library for your symbolic Kontrol tests
Solidity
9
star
34

blockchain-k-plugin

K plugin for IELE and KEVM
C++
8
star
35

bn128-ml

BN 128 elliptic curve implementation in OCAML (for Ethereum zero-knowledge proofs)
OCaml
8
star
36

knock

Nock semantics in K
Python
7
star
37

mx-semantics

Python
7
star
38

rdao-smc

A probabilistic rewriting model of Randao-based RNG schemes
TeX
7
star
39

hs-backend-booster

Accelerates K Framework's Haskell backend
Haskell
7
star
40

proof-generation

Python
6
star
41

kup

K and Semantics Distribution Tool
Python
6
star
42

kavm-demo

Python
6
star
43

rv-android

Android runtime library for the RV-Monitor environment.
Java
5
star
44

match

RV-Match issue tracker and releases
4
star
45

gitbook-kontrol

4
star
46

imp-semantics

The K semantics of IMP and associated tools
Python
4
star
47

predict

3
star
48

vlsm

Coq
3
star
49

property-db

An annotated Java API and a tool for generated documentation augmented with properties.
Java
3
star
50

k-vs-coq-language-frameworks

Coq
3
star
51

pl-tutorial

The K Programming Language Tutorial
Standard ML
3
star
52

rv-predict

Code for improved rv-predict and installer
C
2
star
53

evaluation

Evaluation results of RV tools and comparisons with other tools
Python
2
star
54

rvmatch-eclipse-plugin

Java
2
star
55

kontrol-tutorial

Solidity
2
star
56

khoon

Python
2
star
57

optimism-ci

CI Hosting Symbolic Execution for Ethereum-Optimism
2
star
58

llvmmop

MOP framework for LLVM
Java
2
star
59

CANtools

RV tools for reverse engineering the automotive CAN bus.
1
star
60

rv-toolkit-docs

HTML
1
star
61

racy-c-programs

Benchmark of C/C++ programs exhibiting races.
C++
1
star
62

test-maven-deployment

Test - Delete me
1
star
63

rv-match_testing

Shell
1
star
64

z3k

C++ type inferencer for K using libz3
C++
1
star
65

k-pldi-tutorial

Code supporting K tutorial session at PLDI 2023.
Shell
1
star
66

elrond-multisig

Starlark
1
star
67

gitbook-kevm

1
star
68

proof-checker-public

C++
1
star
69

mir-semantics

Python
1
star
70

kore-prof

Profiling utilities extracted from haskell-backend
Haskell
1
star
71

RV-Log

Frontend for feeding log files and other precomputed event traces to RV-Monitor.
Java
1
star
72

mir-semantics-compiletest

Test suite for MIR semantics
Rust
1
star
73

gitbook-home

1
star
74

riscv-gnu-toolchain-images

Docker image builds for the RISC-V GNU toolchain
Dockerfile
1
star
75

nailgun

Nailgun is a client, protocol, and server for running Java programs from the command line without incurring the JVM startup overhead.
Java
1
star
76

ercx-vscode

VSCode support for ERCx
TypeScript
1
star
77

simbolik-examples

Solidity
1
star
78

rv-install

Unified installer for all Runtime Verification Inc. products
Java
1
star