diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md index d0fb54b86..369fb800b 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md @@ -28,8 +28,5 @@ module BINARY-PARSER-TEST , #module(... metadata: _ => #meta (... id: , funcIds: .Map , filename: "error: test addDefnToModule branch called." ))) [owise] - rule parseSection(U:UnparsedSection) - => parseError("parseSection test default", ListItem(U)) - [owise] endmodule ``` diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md index 8a5e96978..1ab04bfd5 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md @@ -9,8 +9,13 @@ requires "binary-parsing/base.md" requires "binary-parsing/constant.md" requires "binary-parsing/defn.md" requires "binary-parsing/functype.md" +requires "binary-parsing/globaltype.md" +requires "binary-parsing/import.md" +requires "binary-parsing/import-section.md" requires "binary-parsing/int.md" +requires "binary-parsing/limits.md" requires "binary-parsing/module.md" +requires "binary-parsing/name.md" requires "binary-parsing/resulttype.md" requires "binary-parsing/section.md" requires "binary-parsing/tags.md" @@ -30,8 +35,13 @@ module BINARY-PARSER [private] imports BINARY-PARSER-CONSTANT imports BINARY-PARSER-FUNCTYPE + imports BINARY-PARSER-GLOBALTYPE + imports BINARY-PARSER-IMPORT + imports BINARY-PARSER-IMPORT-SECTION imports BINARY-PARSER-INT + imports BINARY-PARSER-LIMITS imports BINARY-PARSER-MODULE + imports BINARY-PARSER-NAME imports BINARY-PARSER-RESULTTYPE imports BINARY-PARSER-SECTION imports BINARY-PARSER-SYNTAX diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/globaltype.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/globaltype.md new file mode 100644 index 000000000..c55cbe8c1 --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/globaltype.md @@ -0,0 +1,41 @@ +Parsing [global types](https://webassembly.github.io/spec/core/binary/types.html#global-types) + +```k +module BINARY-PARSER-GLOBALTYPE-SYNTAX + imports BINARY-PARSER-BASE-SYNTAX + imports WASM + + syntax GlobalTypeResult ::= globalTypeResult(GlobalType, BytesWithIndex) | ParseError + syntax GlobalTypeResult ::= parseGlobalType(BytesWithIndex) [function, total] +endmodule + +module BINARY-PARSER-GLOBALTYPE [private] + imports BINARY-PARSER-CONSTANT-SYNTAX + imports BINARY-PARSER-GLOBALTYPE-SYNTAX + imports BINARY-PARSER-TAGS + imports BINARY-PARSER-VALTYPE-SYNTAX + + syntax GlobalTypeResult ::= #parseGlobalType1(ValTypeResult) [function, total] + | #parseGlobalType2(ValType, MutResult) [function, total] + + rule parseGlobalType(BWI:BytesWithIndex) => #parseGlobalType1(parseValType(BWI)) + rule #parseGlobalType1(valTypeResult(T:ValType, BWI:BytesWithIndex)) + => #parseGlobalType2(T, parseMut(BWI)) + rule #parseGlobalType1(E:ParseError) => E + rule #parseGlobalType2(T:ValType, mutResult(Mut:Mut, BWI:BytesWithIndex)) + => globalTypeResult(Mut T, BWI) + rule #parseGlobalType2(_, E:ParseError) => E + + + syntax MutResult ::= mutResult(Mut, BytesWithIndex) | ParseError + syntax MutResult ::= parseMut(BytesWithIndex) [function, total] + | #parseMut1(BytesWithIndex, BytesWithIndexOrError) [function, total] + | #parseMut2(BytesWithIndexOrError) [function, total] + rule parseMut(BWI:BytesWithIndex) => #parseMut1(BWI, parseConstant(BWI, GLOBAL_CNST)) + rule #parseMut1(_:BytesWithIndex, BWI:BytesWithIndex) => mutResult(const, BWI) + rule #parseMut1(BWI, _:ParseError) => #parseMut2(parseConstant(BWI, GLOBAL_VAR)) + rule #parseMut2(BWI:BytesWithIndex) => mutResult(var, BWI) + rule #parseMut2(E:ParseError) => E + +endmodule +``` diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/import-section.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/import-section.md new file mode 100644 index 000000000..20440ef7f --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/import-section.md @@ -0,0 +1,39 @@ +// Parsing an [import section](https://webassembly.github.io/spec/core/binary/modules.html#binary-importsec). + +```k +module BINARY-PARSER-IMPORT-SECTION-SYNTAX + imports BINARY-PARSER-BASE-SYNTAX + + syntax SectionResult ::= parseImportSection(BytesWithIndex) [function, total] + +endmodule + +module BINARY-PARSER-IMPORT-SECTION [private] + imports BINARY-PARSER-DEFN-SYNTAX + imports BINARY-PARSER-IMPORT-SECTION-SYNTAX + imports BINARY-PARSER-IMPORT-SYNTAX + imports BINARY-PARSER-INT-SYNTAX + imports BINARY-PARSER-SECTION-SYNTAX + + syntax SectionResult ::= #parseImportSection(IntResult) [function, total] + rule parseImportSection(BWI:BytesWithIndex) => #parseImportSection(parseLeb128UInt(BWI)) + rule #parseImportSection(intResult(Count:Int, BWI:BytesWithIndex)) + => parseImportSectionVector(Count, .Defns, BWI) + rule #parseImportSection(E:ParseError) => E + + syntax SectionResult ::= parseImportSectionVector(remainingCount:Int, Defns, BytesWithIndex) [function, total] + | #parseImportSectionVector(remainingCount:Int, Defns, DefnResult) [function, total] + rule parseImportSectionVector(0, D:Defns, BWI:BytesWithIndex) => sectionResult(defnsSection(D), BWI) + rule parseImportSectionVector(Count:Int, D:Defns, BWI:BytesWithIndex) + => #parseImportSectionVector(Count, D, parseImport(BWI)) + requires Count >Int 0 + rule parseImportSectionVector(Count:Int, D:Defns, bwi(B:Bytes, I:Int)) + => parseError("parseImportSectionVector", ListItem(Count) ListItem(D) ListItem(I) ListItem(lengthBytes(B)) ListItem(B)) + [owise] + rule #parseImportSectionVector(Count:Int, Ds:Defns, defnResult(D:Defn, BWI:BytesWithIndex)) + => parseImportSectionVector(Count -Int 1, D Ds, BWI) + rule #parseImportSectionVector(_Count:Int, _:Defns, E:ParseError) => E + + +endmodule +``` diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/import.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/import.md new file mode 100644 index 000000000..15a3512df --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/import.md @@ -0,0 +1,94 @@ +// Parsing an [import](https://webassembly.github.io/spec/core/binary/modules.html#binary-importsec). + +```k +module BINARY-PARSER-IMPORT-SYNTAX + imports BINARY-PARSER-BASE-SYNTAX + + syntax DefnResult ::= parseImport(BytesWithIndex) [function, total] + +endmodule + +module BINARY-PARSER-IMPORT [private] + imports BINARY-PARSER-CONSTANT-SYNTAX + imports BINARY-PARSER-DEFN-SYNTAX + imports BINARY-PARSER-GLOBALTYPE-SYNTAX + imports BINARY-PARSER-IMPORT-SYNTAX + imports BINARY-PARSER-INT-SYNTAX + imports BINARY-PARSER-LIMITS-SYNTAX + imports BINARY-PARSER-NAME-SYNTAX + imports BINARY-PARSER-SECTION-SYNTAX + imports BINARY-PARSER-TAGS + imports BINARY-PARSER-VALTYPE-SYNTAX + imports WASM + + syntax DefnResult ::= #parseImport1(NameResult) [function, total] + | #parseImport2(WasmString, NameResult) [function, total] + | #parseImport3(WasmString, WasmString, ImportDescResult) [function, total] + + rule parseImport(BWI:BytesWithIndex) => #parseImport1(parseName(BWI)) + rule #parseImport1(nameResult(Name:WasmString, BWI:BytesWithIndex)) + => #parseImport2(Name, parseName(BWI)) + rule #parseImport1(E:ParseError) => E + rule #parseImport2(ModuleName:WasmString, nameResult(ObjectName:WasmString, BWI:BytesWithIndex)) + => #parseImport3(ModuleName, ObjectName, parseImportDesc(BWI)) + rule #parseImport2(_, E:ParseError) => E + rule #parseImport3(ModuleName:WasmString, ObjectName:WasmString, importDescResult(Desc:ImportDesc, BWI:BytesWithIndex)) + => defnResult(#import(ModuleName, ObjectName, Desc), BWI) + rule #parseImport3(_, _, E:ParseError) => E + + + syntax ImportDescResult ::= importDescResult(ImportDesc, BytesWithIndex) | ParseError + syntax ImportDescResult ::= parseImportDesc(BytesWithIndex) [function, total] + | #parseImportDescFunc(BytesWithIndex, BytesWithIndexOrError) [function, total] + | #parseImportDescTable(BytesWithIndex, BytesWithIndexOrError) [function, total] + | #parseImportDescMem(BytesWithIndex, BytesWithIndexOrError) [function, total] + | #parseImportDescGlobal(BytesWithIndex, BytesWithIndexOrError) [function, total] + | parseImportDescFunc(IntResult) [function, total] + | parseImportDescTable(ValTypeResult) [function, total] + | #parseImportDescTable1(ValType, LimitsResult) [function, total] + | parseImportDescMem(LimitsResult) [function, total] + | parseImportDescGlobal(GlobalTypeResult) [function, total] + + rule parseImportDesc(BWI:BytesWithIndex) + => #parseImportDescFunc(BWI, parseConstant(BWI, IMPORT_FUNC)) + rule #parseImportDescFunc(_:BytesWithIndex, BWI:BytesWithIndex) + => parseImportDescFunc(parseLeb128UInt(BWI)) + rule #parseImportDescFunc(BWI:BytesWithIndex, _:ParseError) + => #parseImportDescTable(BWI, parseConstant(BWI, IMPORT_TBLT)) + rule #parseImportDescTable(_:BytesWithIndex, BWI:BytesWithIndex) + // TODO: This should use parseRefType in order to properly validate the + // data, but we are dropping the result for now so we're using the + // already implemented parseValType. + => parseImportDescTable(parseValType(BWI)) + rule #parseImportDescTable(BWI:BytesWithIndex, _:ParseError) + => #parseImportDescMem(BWI, parseConstant(BWI, IMPORT_MEMT)) + rule #parseImportDescMem(_:BytesWithIndex, BWI:BytesWithIndex) + => parseImportDescMem(parseLimits(BWI)) + rule #parseImportDescMem(BWI:BytesWithIndex, _:ParseError) + => #parseImportDescGlobal(BWI, parseConstant(BWI, IMPORT_GLBT)) + rule #parseImportDescGlobal(_:BytesWithIndex, BWI:BytesWithIndex) + => parseImportDescGlobal(parseGlobalType(BWI)) + rule #parseImportDescGlobal(_:BytesWithIndex, E:ParseError) => E + + rule parseImportDescFunc(intResult(Value:Int, BWI:BytesWithIndex)) + => importDescResult(#funcDesc(, Value), BWI) + rule parseImportDescFunc(E:ParseError) => E + + rule parseImportDescTable(valTypeResult(Value:ValType, BWI:BytesWithIndex)) + => #parseImportDescTable1(Value, parseLimits(BWI)) + rule parseImportDescTable(E:ParseError) => E + // TODO: Do we need RefType for anything? + rule #parseImportDescTable1(_RefType:ValType, limitsResult(L:Limits, BWI:BytesWithIndex)) + => importDescResult(#tableDesc(, L), BWI) + rule #parseImportDescTable1(_, E:ParseError) => E + + rule parseImportDescMem(limitsResult(L:Limits, BWI:BytesWithIndex)) + => importDescResult(#memoryDesc(, L), BWI) + rule parseImportDescMem(E:ParseError) => E + + rule parseImportDescGlobal(globalTypeResult(GT:GlobalType, BWI:BytesWithIndex)) + => importDescResult(#globalDesc(, GT), BWI) + rule parseImportDescGlobal(E:ParseError) => E + +endmodule +``` diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/limits.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/limits.md new file mode 100644 index 000000000..27172c90f --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/limits.md @@ -0,0 +1,46 @@ +Parsing [limits](https://webassembly.github.io/spec/core/binary/types.html#limits). + +```k + +module BINARY-PARSER-LIMITS-SYNTAX + imports BINARY-PARSER-BASE-SYNTAX + imports WASM-DATA-COMMON + + syntax LimitsResult ::= limitsResult(Limits, BytesWithIndex) | ParseError + syntax LimitsResult ::= parseLimits(BytesWithIndex) [function, total] +endmodule + +module BINARY-PARSER-LIMITS [private] + imports BINARY-PARSER-CONSTANT-SYNTAX + imports BINARY-PARSER-INT-SYNTAX + imports BINARY-PARSER-LIMITS-SYNTAX + imports BINARY-PARSER-TAGS + + syntax LimitsResult ::= #parseLimits1(BytesWithIndex, BytesWithIndexOrError) [function, total] + | #parseLimits2(BytesWithIndexOrError) [function, total] + | parseLimitsMin(IntResult) [function, total] + | parseLimitsMinMax(IntResult) [function, total] + | #parseLimitsMinMax(Int, IntResult) [function, total] + + rule parseLimits(BWI:BytesWithIndex) => #parseLimits1(BWI, parseConstant(BWI, LIMITS_MIN)) + rule #parseLimits1(_:BytesWithIndex, BWI:BytesWithIndex) + => parseLimitsMin(parseLeb128UInt(BWI)) + rule #parseLimits1(BWI:BytesWithIndex, _:ParseError) + => #parseLimits2(parseConstant(BWI, LIMITS)) + rule #parseLimits2(BWI:BytesWithIndex) + => parseLimitsMinMax(parseLeb128UInt(BWI)) + rule #parseLimits2(E:ParseError) => E + + rule parseLimitsMin(intResult(Min:Int, BWI:BytesWithIndex)) + => limitsResult(#limitsMin(Min), BWI) + rule parseLimitsMin(E:ParseError) => E + + rule parseLimitsMinMax(intResult(Min:Int, BWI:BytesWithIndex)) + => #parseLimitsMinMax(Min, parseLeb128UInt(BWI)) + rule parseLimitsMinMax(E:ParseError) => E + rule #parseLimitsMinMax(Min:Int, intResult(Max:Int, BWI:BytesWithIndex)) + => limitsResult(#limits(Min, Max), BWI) + rule #parseLimitsMinMax(_, E:ParseError) => E + +endmodule +``` diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/module.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/module.md index c3b0bee87..8cce0db79 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/module.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/module.md @@ -70,5 +70,7 @@ module BINARY-PARSER-MODULE [private] // addDefnToModule should be called with Defns in reverse order // (the last defn should be processed in the first call). rule addDefnToModule(false => true, T:TypeDefn, #module(... types: Ts => T Ts)) + rule addDefnToModule(false => true, I:ImportDefn, #module(... importDefns: Is => I Is)) + endmodule ``` diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/name.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/name.md new file mode 100644 index 000000000..ec1c51a3c --- /dev/null +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/name.md @@ -0,0 +1,49 @@ +Parsing [names](https://webassembly.github.io/spec/core/binary/values.html#binary-name) + +```k + +module BINARY-PARSER-NAME-SYNTAX + imports BINARY-PARSER-BASE-SYNTAX + imports WASM-DATA-COMMON-SYNTAX + + syntax NameResult ::= nameResult(WasmString, BytesWithIndex) | ParseError + syntax NameResult ::= parseName(BytesWithIndex) [function, total] +endmodule + +module BINARY-PARSER-NAME [private] + imports BINARY-PARSER-INT-SYNTAX + imports BINARY-PARSER-NAME-SYNTAX + imports BOOL + + syntax NameResult ::= #parseName1(IntResult) [function, total] + | #parseName2(String, BytesWithIndex) [function, total] + + rule parseName(BWI:BytesWithIndex) => #parseName1(parseLeb128UInt(BWI)) + + rule #parseName1(intResult(Length:Int, bwi(B:Bytes, Index:Int))) + // TODO: This should be decoded as an UTF-8 string. However, we do not have + // a good option when doing concrete execution. The documentation for + // Bytes2String does not specify an encoding, and decodeBytes is a partial + // function in a symbolic module. + => #parseName2 + ( Bytes2String(substrBytes(B, Index, Index +Int Length)) + , bwi(B, Index +Int Length) + ) + requires 0 <=Int Index andBool Index +Int Length <=Int lengthBytes(B) + rule #parseName1(intResult(Length:Int, bwi(B:Bytes, Index:Int))) + => parseError("#parseName1", ListItem(Length) ListItem(Index) ListItem(lengthBytes(B)) ListItem(B)) + [owise] + rule #parseName1(E:ParseError) => E + + rule #parseName2(S:String, BWI:BytesWithIndex) + => nameResult + ( string2WasmString(S) + , BWI + ) + requires notBool needsWasmEscaping(S) + rule #parseName2(S:String, bwi(B:Bytes, Index:Int)) + => parseError("#parseName2", ListItem(S) ListItem(Index) ListItem(lengthBytes(B)) ListItem(B)) + [owise] + +endmodule +``` diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/section.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/section.md index cb72f09fb..39ff949f4 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/section.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/section.md @@ -26,6 +26,7 @@ endmodule module BINARY-PARSER-SECTION [private] imports BOOL + imports BINARY-PARSER-IMPORT-SECTION-SYNTAX imports BINARY-PARSER-INT-SYNTAX imports BINARY-PARSER-SECTION-SYNTAX imports BINARY-PARSER-TAGS @@ -36,8 +37,10 @@ module BINARY-PARSER-SECTION [private] => sectionResult(customSection(Data), bwi(Data, lengthBytes(Data))) rule parseSection(unparsedSection(TYPE_SEC, Data:Bytes)) => parseTypeSection(bwi(Data, 0)) - // rule parseSection(A) => parseError("parseSection", ListItem(A)) - // [owise] + rule parseSection(unparsedSection(IMPORT_SEC, Data:Bytes)) + => parseImportSection(bwi(Data, 0)) + rule parseSection(A) => parseError("parseSection", ListItem(A)) + [owise] syntax ParsedSectionsResult ::= #parseSections(SectionResult, ParsedSectionsResult) [function, total] diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/tags.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/tags.md index 2ab351a3d..706497a8f 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/tags.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/tags.md @@ -111,8 +111,8 @@ _Limits_ are used to encode the minimum size of memories and tables; a separate form that also specifies a maximum size is available. ```k - syntax Bytes ::= "LIMITS" [macro] rule LIMITS => b"\x00" - syntax Bytes ::= "LIMITS_MAX" [macro] rule LIMITS_MAX => b"\x01" + syntax Bytes ::= "LIMITS_MIN" [macro] rule LIMITS_MIN => b"\x00" + syntax Bytes ::= "LIMITS" [macro] rule LIMITS => b"\x01" ``` _Globals_ may be declared as mutable or immutable. diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/data.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/data.md index 0dffdad7e..3c26e7013 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/data.md @@ -50,6 +50,11 @@ The exception is for characters that are explicitly escaped which can represent | WasmStringToken // ------------------------------------- + // Defined only when `needsWasmEscaping` returns true. + syntax WasmString ::= string2WasmString ( String ) [function] + syntax Bool ::= needsWasmEscaping(String) [function, total] + + syntax WasmStringToken ::= #String2WasmStringToken ( String ) [function, total, hook(STRING.string2token)] syntax String ::= #parseWasmString ( WasmStringToken ) [function, total, hook(STRING.token2string)] // ---------------------------------------------------------------------------------------------------------- @@ -534,7 +539,7 @@ Each call site _must_ ensure that this is desired behavior before using these fu ### Strings -Wasm uses a different character escape rule with K, so we need to define the `unescape` function ourselves. +Wasm uses a different character escape rule than K, so we need to define the `unescape` function ourselves. ```k syntax String ::= unescape(String) [function] @@ -610,6 +615,30 @@ The implementation is not correct for now because the UTF-8 encoding is not impl andBool substrString(S, IDX +Int 1, IDX +Int 2) ==K "u" ``` +The WasmString -> String conversion is not fully defined for now + +```k + + rule string2WasmString(S:String) => #String2WasmStringToken("\"" +String S +String "\"") + requires notBool needsWasmEscaping(S) + + syntax Bool ::= #needsWasmEscaping(String, Int) [function, total] + rule needsWasmEscaping(S) => #needsWasmEscaping(S, 0) + rule #needsWasmEscaping(S, IDX) => false requires IDX =Int lengthString(S) + rule #needsWasmEscaping(S, IDX) => true + requires 0 <=Int IDX + andBool IDX #needsWasmEscaping(S, IDX +Int 1) + [owise] + + syntax Bool ::= charNeedsWasmEscaping(String) [function, total] + rule charNeedsWasmEscaping(S:String) => false + requires " " <=String S andBool ordChar(S) =/=Int 127 andBool S =/=K "\"" andBool S =/=K "\\" + rule charNeedsWasmEscaping(_:String) => true + [owise] +``` + `DataString`, as is defined in the wasm semantics, is a list of `WasmString`s. `#concatDS` concatenates them together into a single string. The strings to connect needs to be unescaped before concatenated, because the `unescape` function removes the quote sign `"` before and after each substring.