diff --git a/ukm-semantics/main/decoding.md b/ukm-semantics/main/decoding.md index 3561da2..8d41757 100644 --- a/ukm-semantics/main/decoding.md +++ b/ukm-semantics/main/decoding.md @@ -1,8 +1,10 @@ ```k +requires "decoding/impl.md" requires "decoding/syntax.md" module UKM-DECODING + imports private UKM-DECODING-IMPL endmodule ``` diff --git a/ukm-semantics/main/decoding/impl.md b/ukm-semantics/main/decoding/impl.md new file mode 100644 index 0000000..631bbe6 --- /dev/null +++ b/ukm-semantics/main/decoding/impl.md @@ -0,0 +1,16 @@ +```k + +module UKM-DECODING-IMPL + imports private COMMON-K-CELL + imports private UKM-DECODING-SYNTAX + imports private UKM-FULL-PREPROCESSED-CONFIGURATION + + syntax UkmFullPreprocessedCell ::= decodeUkmFullPreprocessedCell(Bytes) + [function, hook(ULM.decode)] + + rule + ukmDecodePreprocessedCell(B:Bytes) => .K ... + (_:UkmFullPreprocessedCell => decodeUkmFullPreprocessedCell(B)) +endmodule + +``` diff --git a/ukm-semantics/main/encoding.md b/ukm-semantics/main/encoding.md index 9f08445..eeb1cdf 100644 --- a/ukm-semantics/main/encoding.md +++ b/ukm-semantics/main/encoding.md @@ -1,8 +1,10 @@ ```k +requires "encoding/impl.md" requires "encoding/syntax.md" module UKM-ENCODING + imports private UKM-ENCODING-IMPL endmodule ``` diff --git a/ukm-semantics/main/encoding/impl.md b/ukm-semantics/main/encoding/impl.md new file mode 100644 index 0000000..d0f10b0 --- /dev/null +++ b/ukm-semantics/main/encoding/impl.md @@ -0,0 +1,22 @@ +```k + +module UKM-ENCODING-IMPL + imports private COMMON-K-CELL + imports private BYTES-SYNTAX + imports private UKM-ENCODING-SYNTAX + imports private UKM-FULL-PREPROCESSED-CONFIGURATION + + syntax Bytes ::= encodeUkmFullPreprocessedCell(UkmFullPreprocessedCell) + [function, hook(ULM.encode)] + + rule + + ukmEncodePreprocessedCell + => ukmEncodedPreprocessedCell(encodeUkmFullPreprocessedCell(Cell)) + ... + + Cell:UkmFullPreprocessedCell + +endmodule + +``` diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md index d303075..bd0dab4 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -4,6 +4,7 @@ module UKM-ENCODING-SYNTAX imports BYTES-SYNTAX syntax UKMInstruction ::= "ukmEncodePreprocessedCell" + | ukmEncodedPreprocessedCell(Bytes) endmodule diff --git a/ukm-semantics/targets/testing/configuration.md b/ukm-semantics/targets/testing/configuration.md index 7d3a7c8..cc4bb5c 100644 --- a/ukm-semantics/targets/testing/configuration.md +++ b/ukm-semantics/targets/testing/configuration.md @@ -9,12 +9,16 @@ requires "rust-semantics/test/configuration.md" module COMMON-K-CELL imports private RUST-EXECUTION-TEST-PARSING-SYNTAX imports private RUST-PREPROCESSING-SYNTAX + imports private UKM-ENCODING-SYNTAX imports private UKM-PREPROCESSING-SYNTAX + imports private UKM-TEST-SYNTAX configuration cratesParser($PGM:WrappedCrateList) ~> ukmPreprocessCrates + ~> ukmEncodePreprocessedCell + ~> ukmDecodePreprocessedCell ~> $TEST:ExecutionTest endmodule diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md index 1321ddc..bfd9566 100644 --- a/ukm-semantics/targets/testing/ukm-target.md +++ b/ukm-semantics/targets/testing/ukm-target.md @@ -1,5 +1,7 @@ ```k +requires "../../main/decoding.md" +requires "../../main/encoding.md" requires "../../main/execution.md" requires "../../main/preprocessing.md" requires "../../test/execution.md" @@ -18,6 +20,8 @@ module UKM-TARGET imports private RUST-COMMON imports private RUST-FULL-PREPROCESSING imports private RUST-EXECUTION-TEST + imports private UKM-DECODING + imports private UKM-ENCODING imports private UKM-EXECUTION imports private UKM-PREPROCESSING imports private UKM-TARGET-CONFIGURATION diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index fef9839..b86ed3a 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -5,6 +5,8 @@ module UKM-TEST-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX imports UKM-HOOKS-UKM-SYNTAX + syntax UkmInstruction ::= "ukmDecodePreprocessedCell" + syntax ExecutionItem ::= "mock" "CallData" | "mock" "Caller" | "mock" UkmHook UkmHookResult @@ -19,6 +21,8 @@ endmodule module UKM-TEST-EXECUTION imports private COMMON-K-CELL imports private RUST-EXECUTION-TEST-CONFIGURATION + imports private UKM-DECODING-SYNTAX + imports private UKM-ENCODING-SYNTAX imports private UKM-EXECUTION-SYNTAX imports private UKM-HOOKS-BYTES-CONFIGURATION imports private UKM-HOOKS-BYTES-SYNTAX @@ -27,6 +31,10 @@ module UKM-TEST-EXECUTION imports private UKM-HOOKS-UKM-SYNTAX imports private UKM-TEST-SYNTAX + // Patching the encoding result to decoding for test purposes + rule ukmEncodedPreprocessedCell(B:Bytes) ~> ukmDecodePreprocessedCell + => ukmDecodePreprocessedCell(B) + syntax Mockable ::= UkmHook rule