Build system tweaks (#12)

* Update pyk

* Work in upgrading pyk

* Implement `kimp run`

* Implement `kimp prove`, drop dead code

* Fix sum spec

* . -> .K

* Use `statements.k` in `kimp prove`

* Update `pyk`

* Add top-level make target to build kimp

* Centralize K and pyk versions tag

* Make python3 python

* Implement passing the definition dir as an environment variable

* Find the `k-src` to use as `includes` in `kprove`

* Add install target

* remove old stuff

* Extend .gitignore, add .dockerignore

* Update .dockerignore

* Build kimp into the Docker image

* Re-implement view-kcfg

* Move specs to examples

* Work on installation instructions

.dockerignore

@@ -0,0 +1,8 @@
+**/.krun*
+**/.kprove*
+**/.kimp
+**/dist
+**/kdist
+**/.mypy_cache
+**/.pytest_cache
+**/.venv*

.gitignore

@@ -3,5 +3,9 @@ module-imports-graph.svg
 tests/specs/verification-kompiled/*
 .krun*
 kimp/.kprove*
+.kimp
 *~
 docker/.image
+dist
+kdist
+*venv

Makefile

@@ -1,6 +1,5 @@
-# Latest versions at the time of writing
-K_VERSION   ?= 6.3.25
-PYK_VERSION ?= 0.1.679
+K_VERSION   ?= $(shell cat deps/k_release)
+PYK_VERSION ?= $(shell cat deps/pyk_release)
 KOMPILE     ?= $(shell which kompile)
 
 default: help
@@ -21,10 +20,12 @@ docker/.image: docker/Dockerfile.k+pyk
 K_SOURCES = $(wildcard kimp/k-src/*.k)
 TARGETS   = $(patsubst %.k,.build/%-kompiled,$(notdir $(K_SOURCES)))
 
-build: build-llvm build-haskell
+build: build-llvm build-haskell build-kimp
 
 build-llvm: have-k $(TARGETS:=-llvm)
 build-haskell: have-k $(TARGETS:=-haskell)
+build-kimp: have-k
+	$(MAKE) -C kimp build
 
 .build/%-kompiled-llvm: kimp/k-src/%.k $(K_SOURCES)
 	$(KOMPILE) --output-definition $@ $< -I kimp/k-src --backend llvm

README.md

@@ -8,7 +8,16 @@ KIMP consists of two major components:
 * The K definition of IMP;
 * The `kimp` command-line tool and Python package, that acts as a frontend to the K definition.
 
-## Build instructions
+## Trying it out in `docker` (EASY)
+
+We have prepared a docker image that allows both using `kimp` as-is and hacking on it. Use the following to start a container with an interactive shell:
+
+```
+```
+
+If everything is up and running, feel free to jump straight to the `Usage` section below. If you don't want to use `docker`, read the next section to build `kimp` manually.
+
+## Installation instructions (ADVANCED)
 
 ### Prerequisites
 
@@ -23,18 +32,70 @@ To build the whole codebase, inclusing the `kimp` CLI and the K definition with
 make build
 ```
 
-### Accessing compiled K definitions
+The `kimp` executable is a relatively thin wrapper for a number of generic K tools. These tools need access to the output of the K compiler that were produced at the previous step. The most robust way to point `kimp` to the K compiler output is by setting the following three environment variables:
 
-The definitions are built with `kbuild`, which places the compiled definitions in `~/.kbuild`. To get an exact path to the definition, use:
 ```
-poetry run kbuild which llvm # for LLVM
-poetry run kbuild which haskell # for Haskell
+export KIMP_LLVM_DIR=$(realpath ./kimp/kdist/v6.3.25/llvm)
+export KIMP_HASKELL_DIR=$(realpath ./kimp/kdist/v6.3.25/haskell)
+export KIMP_K_SRC=$(realpath ./kimp/k-src)
 ```
 
-## Usage
+### Installing
 
 After building the project, you can access the `kimp` CLI via `poetry`:
 
 ```
 poetry run kimp --help
 ```
+
+use `poetry shell` to avoid prefixing every command with `poetry run`.
+
+Alternatively, you can install `kimp` with `pip` into a virtual environment:
+
+```
+python -m venv venv
+source venv/bin/activate
+make -C kimp install # this calls pip for you
+```
+
+Within that virtual environment, you can use `kimp` directly.
+
+
+## Usage
+
+`kimp` is intended to demonstrate the two main function of the K framework:
+* running example IMP programs using K's concrete execution backend
+* proving *claims* about IMP programs by executing them with K's symbolic execution backend
+
+Run `kimp --help` to see the available commands and their arguments. Let us now give examples for both concrete executing and proving:
+
+### Concrete execution
+
+```
+kimp run examples/sumto10.imp
+```
+
+this program adds up the natural numbers up to 10 and should give the following output configuration:
+
+```
+<generatedTop>
+  <k>
+    .K
+  </k>
+  <env>
+    k |-> 11
+    n |-> 10
+    sum |-> 55
+  </env>
+</generatedTop>
+```
+
+### Symbolic execution
+
+```
+kimp prove spec
+```
+
+
+
+

deps/k_release

@@ -0,0 +1 @@
+6.3.25

deps/pyk_release

@@ -0,0 +1 @@
+0.1.679

docker/Dockerfile.k+pyk

@@ -9,7 +9,7 @@ ARG PYK_VERSION
 # see https://github.com/boxboat/fixuid
 RUN addgroup --gid 1000 k-group && \
     adduser -uid 1000 --ingroup k-group --home /home/k-user --shell /bin/sh --disabled-password --gecos "" k-user
-RUN apt install -y curl graphviz && \
+RUN apt-get install -y curl graphviz python-is-python3 && \
     USER=k-user && \
     GROUP=k-group && \
     curl -SsL https://github.com/boxboat/fixuid/releases/download/v0.6.0/fixuid-0.6.0-linux-amd64.tar.gz | tar -C /usr/local/bin -xzf - && \
@@ -31,6 +31,12 @@ RUN pip install poetry && \
     make build && \
     pip install dist/*.whl
 
+# install kimp and set env vars for it
+COPY --chown=k-user:k-group ./kimp /home/k-user/kimp-src
+RUN make -C /home/k-user/kimp-src build && make -C /home/k-user/kimp-src install
+ENV KIMP_LLVM_DIR=/home/k-user/kimp-src/kdist/v${K_VERSION}/llvm       \
+    KIMP_HASKELL_DIR=/home/k-user/kimp-src/kdist/v${K_VERSION}/haskell \
+    KIMP_K_SRC=/home/k-user/kimp-src/k-src
 
 ENTRYPOINT ["fixuid", "-q"]
 

kimp/Makefile

@@ -2,13 +2,9 @@ POETRY     := poetry
 POETRY_RUN := $(POETRY) run
 
 
-default: check test-unit
-
-all: check cov
-
 .PHONY: clean
 clean:
-	rm -rf dist .coverage cov-* .mypy_cache .pytest_cache
+	rm -rf dist .mypy_cache .pytest_cache
 	find -type d -name __pycache__ -prune -exec rm -rf {} \;
 
 .PHONY: build
@@ -23,39 +19,10 @@ kbuild-imp: poetry-install
 	$(POETRY) run kbuild kompile llvm
 	$(POETRY) run kbuild kompile haskell
 
-# Tests
-
-TEST_ARGS :=
-
-test: test-all
-
-test-all: poetry-install
-	$(POETRY_RUN) pytest src/tests --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
-
-test-unit: poetry-install
-	$(POETRY_RUN) pytest src/tests/unit --maxfail=1 --verbose $(TEST_ARGS)
-
-test-integration: poetry-install
-	$(POETRY_RUN) pytest src/tests/integration --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
-
-
-# Coverage
-
-COV_ARGS :=
-
-cov: cov-all
-
-cov-%: TEST_ARGS += --cov=kimp --no-cov-on-fail --cov-branch --cov-report=term
-
-cov-all: TEST_ARGS += --cov-report=html:cov-all-html $(COV_ARGS)
-cov-all: test-all
-
-cov-unit: TEST_ARGS += --cov-report=html:cov-unit-html $(COV_ARGS)
-cov-unit: test-unit
-
-cov-integration: TEST_ARGS += --cov-report=html:cov-integration-html $(COV_ARGS)
-cov-integration: test-integration
-
+.PHONY: install
+install: poetry-install
+	$(POETRY) build
+	pip install dist/*.whl
 
 # Checks and formatting
 

kimp/src/kimp/__main__.py

@@ -4,6 +4,7 @@
 import subprocess
 from argparse import ArgumentParser
 from pathlib import Path
+import os
 from typing import TYPE_CHECKING, Any, Final
 
 from pyk.cli.utils import dir_path, file_path
@@ -19,18 +20,47 @@
 _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
 
 
-def kbuild_definition_dir(target: str) -> Path:
-    proc_result = subprocess.run(
-        ['poetry', 'run', 'kbuild', 'which', target],
-        capture_output=True,
-    )
-    if proc_result.returncode:
-        _LOGGER.critical(
-            f'Could not find kbuild definition for target {target}. Run kbuild kompile {target}, or specify --definition-dir.'
+def find_definiton_dir(target: str) -> Path:
+    '''
+    Find the kompiled definiton directory for a `kbuild` target target:
+    * if the KIMP_${target.upper}_DIR is set --- use that
+    * otherwise ask `kbuild`
+    '''
+
+    def kbuild_definition_dir(target: str) -> Path:
+        proc_result = subprocess.run(
+            ['poetry', 'run', 'kbuild', 'which', target],
+            capture_output=True,
         )
-        exit(proc_result.returncode)
+        if proc_result.returncode:
+            _LOGGER.critical(
+                f'Could not find kbuild definition for target {target}. Run kbuild kompile {target}, or specify --definition-dir.'
+            )
+            exit(proc_result.returncode)
+        else:
+            return Path(proc_result.stdout.splitlines()[0].decode())
+
+    env_definition_dir = os.environ.get(f'KIMP_{target.upper()}_DIR')
+    if env_definition_dir:
+        path = Path(env_definition_dir).resolve()
+        _LOGGER.info(f'Using kompiled definiton at {str(path)}')
+        return path
+    else:
+        return kbuild_definition_dir(target)
+
+
+def find_k_src_dir() -> Path:
+    '''
+    A heuristic way to find the the k-src dir with the K sources is located:
+    * if KIMP_K_SRC environment variable is set --- use that
+    * otherwise, use ./k-src and hope it works
+    '''
+    ksrc_dir = os.environ.get(f'KIMP_K_SRC')
+    if ksrc_dir:
+        ksrc_dir = Path(ksrc_dir).resolve()
     else:
-        return Path(proc_result.stdout.splitlines()[0].decode())
+        ksrc_dir = Path('./k-src')
+    return ksrc_dir
 
 
 def main() -> None:
@@ -55,7 +85,7 @@ def exec_run(
 ) -> None:
     krun_output = KRunOutput[output.upper()]
 
-    definition_dir = str(kbuild_definition_dir('llvm'))
+    definition_dir = str(find_definiton_dir('llvm'))
 
     kimp = KIMP(definition_dir, definition_dir)
 
@@ -81,9 +111,11 @@ def exec_prove(
     max_iterations: int,
     max_depth: int,
     ignore_return_code: bool = False,
+    reinit: bool = False,
     **kwargs: Any,
 ) -> None:
-    definition_dir = str(kbuild_definition_dir('haskell'))
+    definition_dir = str(find_definiton_dir('haskell'))
+    k_src_dir = str(find_k_src_dir())
 
     kimp = KIMP(definition_dir, definition_dir)
 
@@ -94,7 +126,8 @@ def exec_prove(
             claim_id=claim_id,
             max_iterations=max_iterations,
             max_depth=max_depth,
-            includes=['k-src'],  # TODO this needs to be more rubust
+            includes=[k_src_dir],
+            reinit=reinit,
         )
     except ValueError as err:
         _LOGGER.critical(err.args)
@@ -118,18 +151,20 @@ def exec_prove(
 #     inline_nodes: bool = False,
 #     **kwargs: Any,
 # ) -> None:
+#     definition_dir = str(find_definiton_dir('haskell'))
 #     kimp = KIMP(definition_dir, definition_dir)
 #     kimp.show_kcfg(spec_module, claim_id, to_module=to_module, inline_nodes=inline_nodes)
 
 
-# def exec_view_kcfg(
-#     definition_dir: str,
-#     spec_module: str,
-#     claim_id: str,
-#     **kwargs: Any,
-# ) -> None:
-#     kimp = KIMP(definition_dir, definition_dir)
-#     kimp.view_kcfg(spec_module, claim_id)
+def exec_view_kcfg(
+    definition_dir: str,
+    spec_module: str,
+    claim_id: str,
+    **kwargs: Any,
+) -> None:
+    definition_dir = str(find_definiton_dir('haskell'))
+    kimp = KIMP(definition_dir, definition_dir)
+    kimp.view_kcfg(spec_module, claim_id)
 
 
 def create_argument_parser() -> ArgumentParser:
@@ -183,7 +218,7 @@ def create_argument_parser() -> ArgumentParser:
     explore_args.add_argument(
         '--max-iterations',
         dest='max_iterations',
-        default=20,
+        default=1000,
         type=int,
         help='Store every Nth state in the CFG for inspection.',
     )