Add CSE verification script with KCFG minimization and K module generation

Makefile

@@ -51,7 +51,8 @@ test-unit:
 
 test-integration: stable-mir-json build
 	$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \
-			--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS)
+			--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal \
+			$(TEST_ARGS)
 
 # Checks and formatting
 

add1_1000time_proof_backup/cse_call_add1_1000time.smir.main.minimized.show

@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: src/rust/library/std/src/rt.rs:194
+│
+│  (156081 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│   function: main
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+

add1_1000time_proof_backup/cse_call_add1_1000time.smir.main.show

@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: src/rust/library/std/src/rt.rs:194
+│
+│  (156081 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│   function: main
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+

add1_1000time_proof_backup/cse_call_add1_1000time.smir.main.summary

@@ -0,0 +1,11 @@
+Proof ID: cse_call_add1_1000time.smir.main
+Times: 1000
+Start Symbol: main
+SMIR File: /Users/steven/Desktop/projs/mir-semantics/kmir/src/tests/integration/data/exec-smir/cse/cse_call_add1_1000time.smir.json
+Proof Passed: True
+Proof Failed: False
+Original Nodes: 3
+Original Edges: 1
+Minimized Nodes: 3
+Minimized Edges: 1
+K Module Name: MAIN-PROOF

add1_1000time_proof_backup/cse_call_add1_1000time.smir.main/kcfg/nodes/2.json

@@ -0,0 +1 @@
+{"id": 2, "cterm": {"config": {"node": "KApply", "label": {"node": "KLabel", "name": "<generatedTop>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<kmir>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<k>", "params": []}, "args": [{"node": "KSequence", "items": [{"node": "KApply", "label": {"node": "KLabel", "name": "#EndProgram_KMIR-CONTROL-FLOW_KItem", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 1}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<retVal>", "params": []}, "args": [{"node": "KVariable", "name": "RETVAL_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<currentFunc>", "params": []}, "args": [{"node": "KVariable", "name": "CURRENTFUNC_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<currentFrame>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<currentBody>", "params": []}, "args": [{"node": "KVariable", "name": "CURRENTBODY_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<caller>", "params": []}, "args": [{"node": "KVariable", "name": "CALLER_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<dest>", "params": []}, "args": [{"node": "KVariable", "name": "DEST_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<target>", "params": []}, "args": [{"node": "KVariable", "name": "TARGET_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<unwind>", "params": []}, "args": [{"node": "KVariable", "name": "UNWIND_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<locals>", "params": []}, "args": [{"node": "KVariable", "name": "LOCALS_CELL_5d410f2a"}], "arity": 1, "variable": false}], "arity": 6, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<stack>", "params": []}, "args": [{"node": "KVariable", "name": "STACK_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<memory>", "params": []}, "args": [{"node": "KVariable", "name": "MEMORY_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<functions>", "params": []}, "args": [{"node": "KVariable", "name": "FUNCTIONS_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<start-symbol>", "params": []}, "args": [{"node": "KVariable", "name": "START_SYMBOL_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<types>", "params": []}, "args": [{"node": "KVariable", "name": "TYPES_CELL_5d410f2a"}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<adt-to-ty>", "params": []}, "args": [{"node": "KVariable", "name": "ADT_TO_TY_CELL_5d410f2a"}], "arity": 1, "variable": false}], "arity": 10, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<generatedCounter>", "params": []}, "args": [{"node": "KVariable", "name": "GENERATEDCOUNTER_CELL_5d410f2a"}], "arity": 1, "variable": false}], "arity": 2, "variable": false}, "constraints": []}, "attrs": ["terminal"]}

kmir/pyproject.toml

@@ -40,6 +40,7 @@ dev = [
     "pytest",
     "pytest-cov",
     "pytest-mock",
+    "pytest-timeout",
     "pytest-xdist",
     "pyupgrade",
 ]

kmir/src/kmir/kdist/mir-semantics/1.txt

@@ -0,0 +1 @@
+#execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandConstant ( constOperand ( ... span: _ , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindZeroSized , ty: ty ( 27 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place ( ... local: local ( 1 ) , projection: .ProjectionElems ) )  .Operands , destination: DEST , target: TARGET , unwind: UNWIND ) , span: _ ) )

kmir/src/kmir/kdist/mir-semantics/2.txt

@@ -0,0 +1 @@
+#execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 56 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) , args: operandMove ( place (... local: local ( 2 ) , projection: .ProjectionElems ) )  .Operands , destination: place (... local: local ( 1 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 57 ) ) )