Georgy/more updates (#15)

* Add message on how to run `kimp view-kcfg`

* Implement `kimp show-kcfg`, make sure `--reinit` works

* Add docker hun image, expand instructions

README.md

@@ -13,8 +13,11 @@ KIMP consists of two major components:
 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:
 
 ```
+docker run --rm -it -v "$PWD":/home/k-user/workspace -u $(id -u):$(id -g) geo2a/bob24:latest /bin/bash
 ```
 
+This command will download the docker image and mount the current working directory under `~/workspace`. You will have write access to the examples from within the container.
+
 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)
@@ -71,6 +74,8 @@ Run `kimp --help` to see the available commands and their arguments. Let us now
 
 ### Concrete execution
 
+The K Framework generates an LLVM interpreter from the language semantics. Let is see what it does on a simple example program:
+
 ```
 kimp run examples/sumto10.imp
 ```
@@ -92,10 +97,25 @@ this program adds up the natural numbers up to 10 and should give the following
 
 ### Symbolic execution
 
+The K Framework is equipped with a symbolic execution backend that can be used to prove properties of programs. The properties to prove are formulated as K claims, and are essentially statements that one state always rewrites to another state if certain conditions hold. An example K claim that formulates an inductive invariant about the summation program we've executed before can be found in `examples/specs/imp-sum-spec.k`. Let us ask the prover to check this claim:
+
+```
+kimp prove examples/specs/imp-sum-spec.k IMP-SUM-SPEC sum-spec
+```
+
+That command would run for some time and output the symbolic execution trace to a file upon completion. We can pretty-print the trace:
+
+```
+kimp show-kcfg IMP-SUM-SPEC sum-spec
+```
+
+or even explore it interactively in a terminal user interface
+
 ```
-kimp prove spec
+kimp view-kcfg IMP-SUM-SPEC sum-spec
 ```
 
 
 
 
+

kimp/src/kimp/__main__.py

@@ -143,17 +143,15 @@ def exec_prove(
             raise
 
 
-# def exec_show_kcfg(
-#     definition_dir: str,
-#     spec_module: str,
-#     claim_id: str,
-#     to_module: bool = False,
-#     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_show_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.show_kcfg(spec_module, claim_id)
 
 
 def exec_view_kcfg(

kimp/src/kimp/kimp.py

@@ -175,23 +175,18 @@ def prove(
     ) -> None:
         include_dirs = [Path(include) for include in includes]
 
-        spec_modules = self.kprove.get_claim_modules(
-            Path(spec_file), spec_module_name=spec_module, include_dirs=include_dirs
+        claims = self.kprove.get_claims(
+            Path(spec_file), spec_module_name=spec_module, claim_labels=[claim_id], include_dirs=include_dirs
         )
+        claim = single(claims)
         spec_label = f'{spec_module}.{claim_id}'
 
         if not reinit and APRProof.proof_data_exists(spec_label, self.proof_dir):
             # load an existing proof (to continue work in it)
             proof = APRProof.read_proof_data(proof_dir=self.proof_dir, id=f'{spec_module}.{claim_id}')
         else:
             # ignore existing proof data and reinitilize it from a claim
-            proofs = APRProof.from_spec_modules(
-                self.kprove.definition,
-                spec_modules,
-                spec_labels=[spec_label],
-                logs={},
-            )
-            proof = single([p for p in proofs if p.id == spec_label])
+            proof = APRProof.from_claim(self.kprove.definition, claim=claim, logs={}, proof_dir=self.proof_dir)
 
         with legacy_explore(
             self.kprove,
@@ -201,24 +196,43 @@ def prove(
             prover = APRProver(proof, kcfg_explore=kcfg_explore, execute_depth=max_depth, cut_point_rules=['IMP.while'])
             prover.advance_proof(max_iterations=max_iterations)
 
-            proof_show = APRProofShow(self.kprove, node_printer=KIMPNodePrinter(kimp=self))
-            res_lines = proof_show.show(
-                proof,
-            )
             print(proof.summary)
-            print(f'Proof data saved to {proof.proof_subdir}')
-            # print('\n'.join(res_lines))
+            print('============================================')
+            print("What's next?: ")
+            print('============================================')
+            print('To inspect the symbolic execution trace interactively, run: ')
+            print(f'  kimp view-kcfg {spec_module} {claim_id}')
+            print('============================================')
+            print('To dump the symbolic execution trace into stdout, run: ')
+            print(f'  kimp show-kcfg {spec_module} {claim_id}')
+            print('============================================')
+            if not proof.passed:
+                print('To retry the failed/pending proof, run : ')
+                print(f'  kimp prove {spec_file} {spec_module} {claim_id}')
+            print('To start the proof from scratch: ')
+            print(f'  kimp prove --reinit {spec_file} {spec_module} {claim_id}')
 
     def view_kcfg(
         self,
         spec_module: str,
         claim_id: str,
     ) -> None:
         proof = APRProof.read_proof_data(proof_dir=self.proof_dir, id=f'{spec_module}.{claim_id}')
-        # proof = read_proof(f'{spec_module}.{claim_id}', proof_dir=self.proof_dir)
         kcfg_viewer = APRProofViewer(proof, self.kprove, node_printer=KIMPNodePrinter(kimp=self))
         kcfg_viewer.run()
 
+    def show_kcfg(
+        self,
+        spec_module: str,
+        claim_id: str,
+    ) -> None:
+        proof = APRProof.read_proof_data(proof_dir=self.proof_dir, id=f'{spec_module}.{claim_id}')
+        proof_show = APRProofShow(self.kprove, node_printer=KIMPNodePrinter(kimp=self))
+        res_lines = proof_show.show(
+            proof,
+        )
+        print('\n'.join(res_lines))
+
     @classmethod
     def _patch_symbol_table(cls, symbol_table: SymbolTable) -> None:
         symbol_table['_Map_'] = paren(lambda m1, m2: m1 + '\n' + m2)