From d0d90aa411db35bae0b72667a4a458c7b0d049c2 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 13 Nov 2023 19:49:48 +1000 Subject: [PATCH 01/15] Added `#halt` rule to signify end of execution. --- kmir/k-src/mir.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/kmir/k-src/mir.md b/kmir/k-src/mir.md index 7643a2aaa..dfaba9618 100644 --- a/kmir/k-src/mir.md +++ b/kmir/k-src/mir.md @@ -56,13 +56,22 @@ The `#halt` construct is used to signify the end of execution. Any remaining ite ```k syntax KItem ::= "#halt" //---------------------- +<<<<<<< HEAD rule [halt]: #halt ~> (_:MirSimulation => .K) rule #halt ~> (#initialized() => .K) +======= + rule [halt]: #halt ~> (_:MirSimulation => .K) ... + rule #halt ~> (#initialized() => .K) ... +>>>>>>> 4c626f2 (Added `#halt` rule to signify end of execution.) endmodule ``` +<<<<<<< HEAD `MIR-SYMBOLIC` is a stub module to be used with the Haskell backend in the future. It does not import `MIR-AMBIGUITIES`, since `amb` productions are not supported by the Haskell backend. We may need to consult the C semantics team when we start working on symbolic execution. +======= +`MIR-SYMBOLIC` is a stub module to be used with the Haskell backend in the future. It does not import `MIR-AMBIGUITIES`, since the `amb` productions seem to not be supported by the Haskell backend. We may need to consult the C semantics team when we start working on symbolic execution. +>>>>>>> 4c626f2 (Added `#halt` rule to signify end of execution.) ```k module MIR-SYMBOLIC From 07d64c25dadf6e77886fa8f32f330e8d292916fa Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 13 Nov 2023 22:08:25 +1000 Subject: [PATCH 02/15] [BROKEN] Added `KMIRSemantics` with explicit terminal rules. Error occurs from `pyk` internal call to `is_terminal` --- kmir/k-src/mir.md | 9 --------- 1 file changed, 9 deletions(-) diff --git a/kmir/k-src/mir.md b/kmir/k-src/mir.md index dfaba9618..7643a2aaa 100644 --- a/kmir/k-src/mir.md +++ b/kmir/k-src/mir.md @@ -56,22 +56,13 @@ The `#halt` construct is used to signify the end of execution. Any remaining ite ```k syntax KItem ::= "#halt" //---------------------- -<<<<<<< HEAD rule [halt]: #halt ~> (_:MirSimulation => .K) rule #halt ~> (#initialized() => .K) -======= - rule [halt]: #halt ~> (_:MirSimulation => .K) ... - rule #halt ~> (#initialized() => .K) ... ->>>>>>> 4c626f2 (Added `#halt` rule to signify end of execution.) endmodule ``` -<<<<<<< HEAD `MIR-SYMBOLIC` is a stub module to be used with the Haskell backend in the future. It does not import `MIR-AMBIGUITIES`, since `amb` productions are not supported by the Haskell backend. We may need to consult the C semantics team when we start working on symbolic execution. -======= -`MIR-SYMBOLIC` is a stub module to be used with the Haskell backend in the future. It does not import `MIR-AMBIGUITIES`, since the `amb` productions seem to not be supported by the Haskell backend. We may need to consult the C semantics team when we start working on symbolic execution. ->>>>>>> 4c626f2 (Added `#halt` rule to signify end of execution.) ```k module MIR-SYMBOLIC From 8ec8d4c2ac482b5ecdce499cf69fbae17d4c7552 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 17 Nov 2023 08:53:58 +1000 Subject: [PATCH 03/15] Added booster as backend target --- kmir/k-src/mir.md | 1 - kmir/src/kmir/__main__.py | 10 ++++++++++ kmir/src/kmir/cli.py | 12 ++++++++++++ 3 files changed, 22 insertions(+), 1 deletion(-) diff --git a/kmir/k-src/mir.md b/kmir/k-src/mir.md index 7643a2aaa..cacc6688d 100644 --- a/kmir/k-src/mir.md +++ b/kmir/k-src/mir.md @@ -61,7 +61,6 @@ The `#halt` construct is used to signify the end of execution. Any remaining ite endmodule ``` - `MIR-SYMBOLIC` is a stub module to be used with the Haskell backend in the future. It does not import `MIR-AMBIGUITIES`, since `amb` productions are not supported by the Haskell backend. We may need to consult the C semantics team when we start working on symbolic execution. ```k diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 6b0c5fd0a..fb9528ff6 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -104,6 +104,8 @@ def exec_prove( definition_dir: str, haskell_dir: str, spec_file: str, + *, + use_booster: bool = False, bug_report: bool = False, save_directory: Path | None = None, reinit: bool = False, @@ -111,6 +113,7 @@ def exec_prove( smt_timeout: int | None = None, smt_retry_limit: int | None = None, trace_rewrites: bool = False, + kore_rpc_command: str | Iterable[str] | None = None, **kwargs: Any, ) -> None: if spec_file is None: @@ -134,6 +137,11 @@ def exec_prove( if not claims: raise ValueError(f'No claims found in file {spec_file}') + if kore_rpc_command is None: + kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',) + elif isinstance(kore_rpc_command, str): + kore_rpc_command = kore_rpc_command.split() + def is_functional(claim: KClaim) -> bool: claim_lhs = claim.body if type(claim_lhs) is KRewrite: @@ -145,7 +153,9 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: kprove, kcfg_semantics=KMIRSemantics(), id=claim.label, + llvm_definition_dir=kmir.llvm_dir, bug_report=br, + kore_rpc_command=kore_rpc_command, smt_timeout=smt_timeout, smt_retry_limit=smt_retry_limit, trace_rewrites=trace_rewrites, diff --git a/kmir/src/kmir/cli.py b/kmir/src/kmir/cli.py index 401100531..76e61adfe 100644 --- a/kmir/src/kmir/cli.py +++ b/kmir/src/kmir/cli.py @@ -157,6 +157,18 @@ def create_argument_parser() -> ArgumentParser: default=False, help='Reinitialise a proof.', ) + prove_subparser.add_argument( + '--use-booster', + action='store_true', + default=False, + help='Use the booster backend instead of the haskell backend', + ) + prove_subparser.add_argument( + '--kore-rpc-command', + type=str, + default=None, + help='Custom command to start RPC server', + ) kmir_cli_args = KMIRCLIArgs() From e61684c21258d88f8abf179c3da312c8f9810ad4 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 17 Nov 2023 12:17:19 +1000 Subject: [PATCH 04/15] Added `runLemma` `doneLemma` paradigm --- kmir/k-src/mir.md | 5 +++++ kmir/src/tests/integration/proofs/lemmas.k | 21 +++++++++++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 kmir/src/tests/integration/proofs/lemmas.k diff --git a/kmir/k-src/mir.md b/kmir/k-src/mir.md index cacc6688d..694a6e08c 100644 --- a/kmir/k-src/mir.md +++ b/kmir/k-src/mir.md @@ -70,6 +70,11 @@ module MIR-SYMBOLIC imports MIR-EXECUTION imports MIR-FINALIZATION + syntax KItem ::= runLemma ( Step ) | doneLemma ( Step ) + // ------------------------------------------------------- + rule runLemma(S) => doneLemma(S) ... + + syntax Step ::= Bool | Int | MIRValue endmodule ``` diff --git a/kmir/src/tests/integration/proofs/lemmas.k b/kmir/src/tests/integration/proofs/lemmas.k new file mode 100644 index 000000000..0e3bb503b --- /dev/null +++ b/kmir/src/tests/integration/proofs/lemmas.k @@ -0,0 +1,21 @@ +requires "../../../../k-src/mir.md" + +module VERIFICATION + imports K-EQUAL + imports BASIC-K + imports MIR-SYMBOLIC + + // LocalTokens will have parsing error if they are not enumerated here + syntax LocalToken ::= "_1" [token] + syntax LocalToken ::= "_2" [token] + syntax LocalToken ::= "_3" [token] + syntax LocalToken ::= "_4" [token] +endmodule + +module LEMMAS + imports VERIFICATION + + // For testing + claim runLemma(isRValueResult(_:RValueResult)) => doneLemma(true) ... + claim runLemma(isRValueResult(_:MIRValue)) => doneLemma(true) ... +endmodule \ No newline at end of file From 39bcbbe398ce6a84be90cad8e6930a4d4944f124 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 17 Nov 2023 12:31:24 +1000 Subject: [PATCH 05/15] added simplify init --- kmir/src/kmir/__main__.py | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index fb9528ff6..bdf4fcdb7 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -5,6 +5,7 @@ from pathlib import Path from typing import Any, Final +from pyk.cterm import CTerm from pyk.kast.outer import KApply, KClaim, KRewrite from pyk.kcfg import KCFG from pyk.ktool.kprint import KAstInput, KAstOutput @@ -153,14 +154,13 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: kprove, kcfg_semantics=KMIRSemantics(), id=claim.label, - llvm_definition_dir=kmir.llvm_dir, + llvm_definition_dir=kmir.llvm_dir if use_booster else None, bug_report=br, kore_rpc_command=kore_rpc_command, smt_timeout=smt_timeout, smt_retry_limit=smt_retry_limit, trace_rewrites=trace_rewrites, ) as kcfg_explore: - # TODO: simplfy_init proof_problem: Proof if is_functional(claim): if ( @@ -185,6 +185,14 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}') new_init = kcfg_explore.cterm_assume_defined(new_init) + _LOGGER.info(f'Simplifying initial and target node: {claim.label}') + new_init, _ = kcfg_explore.cterm_simplify(new_init) + new_target, _ = kcfg_explore.cterm_simplify(new_target) + if CTerm._is_bottom(new_init.kast): + raise ValueError('Simplifying initial node led to #Bottom, are you sure your LHS is defined?') + if CTerm._is_top(new_target.kast): + raise ValueError('Simplifying target node led to #Bottom, are you sure your RHS is defined?') + kcfg.replace_node(init_node_id, new_init) kcfg.replace_node(target_node_id, new_target) From edaa357b5a39fbdb0815fc35ea9d6e5a07d1691b Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 17 Nov 2023 12:39:28 +1000 Subject: [PATCH 06/15] failing proof working again --- .../tests/integration/proofs/simple-spec.k | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/kmir/src/tests/integration/proofs/simple-spec.k b/kmir/src/tests/integration/proofs/simple-spec.k index a317de4a0..97b0edead 100644 --- a/kmir/src/tests/integration/proofs/simple-spec.k +++ b/kmir/src/tests/integration/proofs/simple-spec.k @@ -84,20 +84,20 @@ module SIMPLE-SPEC requires INDEX ==Int Local2Int(PLACE) - // claim #executeStatement(_1:Local = move _2) => .K ... - // ListItem(FN_KEY) ... - // - // FN_KEY - // - // 1 - // _ => 42 - // ... - // - // - // 2 - // 42 - // ... - // - // ... - // + claim #executeStatement(_1:Local = move _2) => .K ... + ListItem(FN_KEY) ... + + FN_KEY + + 1 + _ => 42 + ... + + + 2 + 42 + ... + + ... + endmodule \ No newline at end of file From 24755afd2c70e10a0d5a622df1e343149ce974d7 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 17 Nov 2023 20:04:37 +1000 Subject: [PATCH 07/15] Fixed proof failure information --- kmir/src/kmir/utils.py | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py index 35537bba4..05649cca0 100644 --- a/kmir/src/kmir/utils.py +++ b/kmir/src/kmir/utils.py @@ -197,12 +197,8 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_i simplified_node, _ = kcfg_explore.cterm_simplify(node.cterm) simplified_target, _ = kcfg_explore.cterm_simplify(target.cterm) - # TODO: Remove the ignore annotations, unsure why mypy couldn't infer type here - node_cterm = CTerm.from_kast(simplified_node) # type: ignore - target_cterm = CTerm.from_kast(simplified_target) # type: ignore - res_lines.append(' Failure reason:') - _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) + _, reason = kcfg_explore.implication_failure_reason(simplified_node, simplified_target) res_lines += [f' {line}' for line in reason.split('\n')] res_lines.append(' Path condition:') From 2d4f13dacbf7a0ca578b6bae42683b49e99162c2 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 17 Nov 2023 20:07:10 +1000 Subject: [PATCH 08/15] Moved halt rules so that SYMBOLIC module could see them --- kmir/k-src/mir.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/kmir/k-src/mir.md b/kmir/k-src/mir.md index 694a6e08c..1d42bc6d2 100644 --- a/kmir/k-src/mir.md +++ b/kmir/k-src/mir.md @@ -49,15 +49,6 @@ If we are, then we stop execution and enter the finalization phase. Otherwise, i rule #return(FUNCTION_KEY, _) => .K ... ListItem(FUNCTION_KEY) XS => XS requires FUNCTION_KEY =/=K Fn(main) -``` - -The `#halt` construct is used to signify the end of execution. Any remaining items on the `` cell will be removed. - -```k - syntax KItem ::= "#halt" - //---------------------- - rule [halt]: #halt ~> (_:MirSimulation => .K) - rule #halt ~> (#initialized() => .K) endmodule ``` @@ -316,6 +307,15 @@ module MIR-EXECUTION imports K-EQUAL ``` +The `#halt` construct is used to signify the end of execution. Any remaining items on the `` cell will be removed. + +```k + syntax KItem ::= "#halt" + //---------------------- + rule [halt]: #halt ~> (_:MirSimulation => .K) + // rule #halt ~> (#initialized() => .K) +``` + Executing a function-like means: * instantiating its arguments in the context of the caller * executing its first basic block From cd948ee5f1cc1750240d804eb4a9a72589feea5b Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 17 Nov 2023 20:08:08 +1000 Subject: [PATCH 09/15] Added empty start-finish MIR program for verification --- .../tests/integration/proofs/empty-program.k | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 kmir/src/tests/integration/proofs/empty-program.k diff --git a/kmir/src/tests/integration/proofs/empty-program.k b/kmir/src/tests/integration/proofs/empty-program.k new file mode 100644 index 000000000..6ad833c58 --- /dev/null +++ b/kmir/src/tests/integration/proofs/empty-program.k @@ -0,0 +1,29 @@ +requires "../../../../k-src/mir.md" + +module VERIFICATION + imports K-EQUAL + imports BASIC-K + imports MIR-SYMBOLIC + + // LocalTokens will have parsing error if they are not enumerated here + syntax LocalToken ::= "_1" [token] + syntax LocalToken ::= "_2" [token] + syntax LocalToken ::= "_3" [token] + syntax LocalToken ::= "_4" [token] + + syntax BBId ::= "bb0" [token] +endmodule + +module EMPTY-PROGRAM + imports VERIFICATION + + claim + + fn main :: .FunctionPath ( .ParameterList ) -> ( ) { .DebugList let mut _0 : ( ) ; .BindingList .ScopeList bb0 : { .Statements return ; } .BasicBlockList } .Mir ~> . + => + #halt ~> . + + .List + 4 => 0 + Initialization => Execution +endmodule \ No newline at end of file From b8977d9253f64a3c684b7fc72b8785f869d3eae7 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 20 Nov 2023 12:16:18 +1000 Subject: [PATCH 10/15] Moved `#halt` back to `MIR` and `MIR-SYMBOLIC` now imports `MIR` --- kmir/k-src/mir.md | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/kmir/k-src/mir.md b/kmir/k-src/mir.md index 1d42bc6d2..772794b8e 100644 --- a/kmir/k-src/mir.md +++ b/kmir/k-src/mir.md @@ -45,10 +45,23 @@ If we are, then we stop execution and enter the finalization phase. Otherwise, i ListItem(Fn(main)) => .List Execution => Finalization _ => 0 + rule #return(Fn(main :: .FunctionPath), Unit) => #halt ... + ListItem(Fn(main)) => .List + Execution => Finalization + _ => 0 rule #return(FUNCTION_KEY, _) => .K ... ListItem(FUNCTION_KEY) XS => XS requires FUNCTION_KEY =/=K Fn(main) +``` + +The `#halt` construct is used to signify the end of execution. Any remaining items on the `` cell will be removed. + +```k + syntax KItem ::= "#halt" + //---------------------- + rule [halt]: #halt ~> (_:MirSimulation => .K) + rule #halt ~> (#initialized() => .K) endmodule ``` @@ -56,10 +69,11 @@ endmodule ```k module MIR-SYMBOLIC - imports MIR-CONFIGURATION - imports MIR-INITIALIZATION - imports MIR-EXECUTION - imports MIR-FINALIZATION + // imports MIR-CONFIGURATION + // imports MIR-INITIALIZATION + // imports MIR-EXECUTION + // imports MIR-FINALIZATION + imports MIR syntax KItem ::= runLemma ( Step ) | doneLemma ( Step ) // ------------------------------------------------------- @@ -307,15 +321,6 @@ module MIR-EXECUTION imports K-EQUAL ``` -The `#halt` construct is used to signify the end of execution. Any remaining items on the `` cell will be removed. - -```k - syntax KItem ::= "#halt" - //---------------------- - rule [halt]: #halt ~> (_:MirSimulation => .K) - // rule #halt ~> (#initialized() => .K) -``` - Executing a function-like means: * instantiating its arguments in the context of the caller * executing its first basic block From 1cb379dfe25f45c96ad7f881717b3be7d9badc54 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 20 Nov 2023 12:18:51 +1000 Subject: [PATCH 11/15] Corrected empty-program.k and added Rust and Mir for it --- kmir/src/tests/integration/proofs/empty-program.k | 3 ++- kmir/src/tests/integration/proofs/empty-program.mir | 9 +++++++++ kmir/src/tests/integration/proofs/empty-program.rs | 3 +++ 3 files changed, 14 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/proofs/empty-program.mir create mode 100644 kmir/src/tests/integration/proofs/empty-program.rs diff --git a/kmir/src/tests/integration/proofs/empty-program.k b/kmir/src/tests/integration/proofs/empty-program.k index 6ad833c58..0cf76ad78 100644 --- a/kmir/src/tests/integration/proofs/empty-program.k +++ b/kmir/src/tests/integration/proofs/empty-program.k @@ -25,5 +25,6 @@ module EMPTY-PROGRAM .List 4 => 0 - Initialization => Execution + Initialization => Finalization + .Bag => ?_ endmodule \ No newline at end of file diff --git a/kmir/src/tests/integration/proofs/empty-program.mir b/kmir/src/tests/integration/proofs/empty-program.mir new file mode 100644 index 000000000..b40ec0f11 --- /dev/null +++ b/kmir/src/tests/integration/proofs/empty-program.mir @@ -0,0 +1,9 @@ +// WARNING: This output format is intended for human consumers only +// and is subject to change without notice. Knock yourself out. +fn main() -> () { + let mut _0: (); + + bb0: { + return; + } +} diff --git a/kmir/src/tests/integration/proofs/empty-program.rs b/kmir/src/tests/integration/proofs/empty-program.rs new file mode 100644 index 000000000..341c018a1 --- /dev/null +++ b/kmir/src/tests/integration/proofs/empty-program.rs @@ -0,0 +1,3 @@ +fn main() { + 42; +} \ No newline at end of file From 8cd3f2e492d722eb8fbdb7866b5c841f2fb35168 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 20 Nov 2023 12:37:53 +1000 Subject: [PATCH 12/15] Added naming to proofs in simple-spec.k --- .../tests/integration/proofs/simple-spec.k | 40 +++++++++---------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/kmir/src/tests/integration/proofs/simple-spec.k b/kmir/src/tests/integration/proofs/simple-spec.k index 97b0edead..0ed05c12d 100644 --- a/kmir/src/tests/integration/proofs/simple-spec.k +++ b/kmir/src/tests/integration/proofs/simple-spec.k @@ -15,7 +15,7 @@ endmodule module SIMPLE-SPEC imports VERIFICATION - claim #executeStatement(_3 = const 5_usize) => .K ... + claim [statement.1]: #executeStatement(_3 = const 5_usize) => .K ... ListItem(FN_KEY) ... FN_KEY @@ -27,7 +27,7 @@ module SIMPLE-SPEC ... - claim #executeStatement(PLACE:Local = const 5_usize) => .K ... + claim [statement.2]: #executeStatement(PLACE:Local = const 5_usize) => .K ... ListItem(FN_KEY) ... FN_KEY @@ -40,7 +40,7 @@ module SIMPLE-SPEC requires INDEX ==Int Local2Int(PLACE) - claim #executeStatement(PLACE:Local = Add(const 3_i32, const 5_i32)) => .K ... + claim [statement.3]: #executeStatement(PLACE:Local = Add(const 3_i32, const 5_i32)) => .K ... ListItem(FN_KEY) ... FN_KEY @@ -53,51 +53,51 @@ module SIMPLE-SPEC requires INDEX ==Int Local2Int(PLACE) - claim #executeStatements(PLACE1:Local = Add(const 3_i32, const 5_i32); PLACE2:Local = Add(const 3_i32, const 6_i32);) => .K ... + claim [statement.4]: #executeStatement(_1:Local = move _2) => .K ... ListItem(FN_KEY) ... FN_KEY - INDEX1 - _ => 8 + 1 + _ => 42 ... - INDEX2 - _ => 9 + 2 + 42 ... ... - requires INDEX1 ==Int Local2Int(PLACE1) andBool INDEX2 ==Int Local2Int(PLACE2) andBool INDEX1 =/=Int INDEX2 - claim #executeStatements(PLACE:Local = Add(const 3_i32, const 5_i32); PLACE:Local = Add(const 3_i32, const 6_i32);) => .K ... + claim [statements.1]: #executeStatements(PLACE1:Local = Add(const 3_i32, const 5_i32); PLACE2:Local = Add(const 3_i32, const 6_i32);) => .K ... ListItem(FN_KEY) ... FN_KEY - INDEX + INDEX1 + _ => 8 + ... + + + INDEX2 _ => 9 ... ... - requires INDEX ==Int Local2Int(PLACE) + requires INDEX1 ==Int Local2Int(PLACE1) andBool INDEX2 ==Int Local2Int(PLACE2) andBool INDEX1 =/=Int INDEX2 - claim #executeStatement(_1:Local = move _2) => .K ... + claim [statements.2]: #executeStatements(PLACE:Local = Add(const 3_i32, const 5_i32); PLACE:Local = Add(const 3_i32, const 6_i32);) => .K ... ListItem(FN_KEY) ... FN_KEY - 1 - _ => 42 - ... - - - 2 - 42 + INDEX + _ => 9 ... ... + requires INDEX ==Int Local2Int(PLACE) endmodule \ No newline at end of file From 236a2c22dec6c948d8e9d077b8aeb20437c4157d Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 20 Nov 2023 13:12:39 +1000 Subject: [PATCH 13/15] added empty-program.k to CI --- kmir/src/tests/integration/test_prove.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kmir/src/tests/integration/test_prove.py b/kmir/src/tests/integration/test_prove.py index 18018a722..25dd51272 100644 --- a/kmir/src/tests/integration/test_prove.py +++ b/kmir/src/tests/integration/test_prove.py @@ -19,8 +19,9 @@ TEST_DIR: Final = REPO_ROOT / 'kmir/src/tests' SYMBOLIC_TEST_DIR: Final = TEST_DIR / 'integration/proofs' INITIAL_SPECS: Final = SYMBOLIC_TEST_DIR / 'simple-spec.k' +EMPTY_PROGRAM: Final = SYMBOLIC_TEST_DIR / 'empty-program.k' -ALL_TESTS: Final = [INITIAL_SPECS] +ALL_TESTS: Final = [INITIAL_SPECS, EMPTY_PROGRAM] def exclude_list(exclude_file: Path) -> list[Path]: @@ -40,7 +41,7 @@ def exclude_list(exclude_file: Path) -> list[Path]: @pytest.mark.parametrize( 'spec_file', ALL_TESTS, - ids=[str(spec_file.relative_to(INITIAL_SPECS)) for spec_file in ALL_TESTS], + ids=[str(spec_file.relative_to(SYMBOLIC_TEST_DIR)) for spec_file in ALL_TESTS], ) def test_pyk_prove( llvm_dir: str, From 47014fe403abe0f8287ff91507af2aeb7cecd163 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 20 Nov 2023 13:31:14 +1000 Subject: [PATCH 14/15] removed duplicate rule in `MIR` module --- kmir/k-src/mir.md | 5 ----- 1 file changed, 5 deletions(-) diff --git a/kmir/k-src/mir.md b/kmir/k-src/mir.md index 772794b8e..2de367e8e 100644 --- a/kmir/k-src/mir.md +++ b/kmir/k-src/mir.md @@ -45,11 +45,6 @@ If we are, then we stop execution and enter the finalization phase. Otherwise, i ListItem(Fn(main)) => .List Execution => Finalization _ => 0 - rule #return(Fn(main :: .FunctionPath), Unit) => #halt ... - ListItem(Fn(main)) => .List - Execution => Finalization - _ => 0 - rule #return(FUNCTION_KEY, _) => .K ... ListItem(FUNCTION_KEY) XS => XS requires FUNCTION_KEY =/=K Fn(main) From 95562f6ba564a0c7144d2e12f9547523409b1438 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Tue, 21 Nov 2023 20:17:43 +1000 Subject: [PATCH 15/15] removing commented out imports --- kmir/k-src/mir.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/kmir/k-src/mir.md b/kmir/k-src/mir.md index 2de367e8e..c281e8804 100644 --- a/kmir/k-src/mir.md +++ b/kmir/k-src/mir.md @@ -64,10 +64,6 @@ endmodule ```k module MIR-SYMBOLIC - // imports MIR-CONFIGURATION - // imports MIR-INITIALIZATION - // imports MIR-EXECUTION - // imports MIR-FINALIZATION imports MIR syntax KItem ::= runLemma ( Step ) | doneLemma ( Step )