diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 19086168a..329735b16 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -86,7 +86,7 @@ jobs: with: container-name: kwasm-ci-parse-${{ github.sha }} - name: 'Build LLVM Backend and pykwasm' - run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} make -j2 build-llvm + run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} make -j2 build-llvm RELEASE=true - name: 'Conformance parse' run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} make test-conformance-parse - name: 'Tear down Docker' @@ -116,7 +116,7 @@ jobs: with: container-name: kwasm-ci-conformance-${{ github.sha }} - name: 'Build LLVM Backend' - run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 build-llvm + run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 build-llvm RELEASE=true - name: 'Simple tests' run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 TEST_CONCRETE_BACKEND=llvm test-simple - name: 'Conformance run' diff --git a/Makefile b/Makefile index 768ac21d9..bd2bc7f71 100644 --- a/Makefile +++ b/Makefile @@ -74,7 +74,7 @@ ALL_SOURCE_FILES := $(patsubst %, %.md, $(SOURCE_FILES)) $(EXTRA_SOURCE_FILES) build: build-llvm build-haskell build-wrc20 ifneq (,$(RELEASE)) - KOMPILE_OPTS += -O2 + KOMPILE_OPTS += -O2 --gen-glr-bison-parser else KOMPILE_OPTS += --debug endif diff --git a/auxil.md b/auxil.md index f84d19dcf..10f77f999 100644 --- a/auxil.md +++ b/auxil.md @@ -6,14 +6,20 @@ Generally useful commands that are not part of the actual Wasm semantics. ```k require "wasm.md" -module WASM-AUXIL - imports WASM +module WASM-AUXIL-SYNTAX + imports WASM-SYNTAX syntax Stmt ::= Auxil // --------------------- syntax Auxil ::= "#clearConfig" // ------------------------------- +endmodule + +module WASM-AUXIL + imports WASM-AUXIL-SYNTAX + imports WASM + rule [clearConfig]: #clearConfig => . ... _ => .Int diff --git a/data.md b/data.md index ed4a1b0ef..5592aa97c 100644 --- a/data.md +++ b/data.md @@ -145,9 +145,81 @@ endmodule `WASM-DATA` module ------------------ +```k +module WASM-DATA-INTERNAL-SYNTAX + imports WASM-DATA-COMMON-SYNTAX + + syntax ValStack ::= ".ValStack" [klabel(.ValStack), symbol] + | Val ":" ValStack [klabel(concatValStack), symbol] +``` + +### Values + +Proper values are numbers annotated with their types. + +```k + syntax IVal ::= "<" IValType ">" Int [klabel(<_>_)] + syntax FVal ::= "<" FValType ">" Float [klabel(<_>_)] + syntax Val ::= "<" ValType ">" Number [klabel(<_>_)] + | IVal | FVal + // --------------------------- +``` + +We also add `undefined` as a value, which makes many partial functions in the semantics total. + +```k + syntax Val ::= "undefined" + // -------------------------- +``` + +### Type Constructors + +There are two basic type-constructors: sequencing (`[_]`) and function spaces (`_->_`). + +```k + syntax VecType ::= "[" ValTypes "]" [klabel(aVecType), symbol] + + syntax FuncType ::= VecType "->" VecType [klabel(aFuncType), symbol] +``` + +All told, a `Type` can be a value type, vector of types, or function type. + +```k + syntax Type ::= ".Type" | ValType | VecType | FuncType +``` + +### OptionalInt + +In some cases, an integer is optional, such as when either giving or omitting the max bound when defining a table or memory. +The sort `OptionalInt` provides this potentially "undefined" `Int`. + +```k + syntax OptionalInt ::= Int | ".Int" [klabel(.Int), symbol] +``` + +### Integer bounds + +```k + syntax Int ::= #pow ( IValType ) [function, total, smtlib(pow )] /* 2 ^Int #width(T) */ + | #pow1 ( IValType ) [function, total, smtlib(pow1)] /* 2 ^Int (#width(T) -Int 1) */ +``` + +### Integer interpretation + +```k + syntax Int ::= #signed ( IValType , Int ) [function] + | #unsigned ( IValType , Int ) [function] + | #signedWidth ( Int , Int ) [function] +``` + +```k +endmodule +``` + ```k module WASM-DATA-COMMON imports WASM-DATA-COMMON-SYNTAX + imports WASM-DATA-INTERNAL-SYNTAX imports INT imports BOOL @@ -219,16 +291,6 @@ For `Int`, however, a the context is irrelevant and the index always just resolv rule elemSegment2Ints(E:Int ES) => E elemSegment2Ints(ES) ``` -### OptionalInt - -In some cases, an integer is optional, such as when either giving or omitting the max bound when defining a table or memory. -The sort `OptionalInt` provides this potentially "undefined" `Int`. - -```k - syntax OptionalInt ::= Int | ".Int" [klabel(.Int), symbol] - // ----------------------------------- -``` - ### Limits Tables and memories have limits, defined as either a single `Int` or two `Int`s, representing min and max bounds. @@ -241,28 +303,14 @@ Tables and memories have limits, defined as either a single `Int` or two `Int`s, ### Type Constructors -There are two basic type-constructors: sequencing (`[_]`) and function spaces (`_->_`). ```k - syntax VecType ::= "[" ValTypes "]" [klabel(aVecType), symbol] - // --------------------------------------------------------------- - - syntax FuncType ::= VecType "->" VecType [klabel(aFuncType), symbol] - // -------------------------------------------------------------------- - syntax Int ::= lengthValTypes ( ValTypes ) [function, total] // ----------------------------------------------------------------- rule lengthValTypes(.ValTypes) => 0 rule lengthValTypes(_V VS) => 1 +Int lengthValTypes(VS) ``` -All told, a `Type` can be a value type, vector of types, or function type. - -```k - syntax Type ::= ".Type" | ValType | VecType | FuncType - // ------------------------------------------------------ -``` - We can append two `ValTypes`s with the `_+_` operator. ```k @@ -301,9 +349,6 @@ The `#width` function returns the bit-width of a given `IValType`. `2 ^Int 32` and `2 ^Int 64` are used often enough to warrant providing helpers for them. ```k - syntax Int ::= #pow ( IValType ) [function, total, smtlib(pow )] /* 2 ^Int #width(T) */ - | #pow1 ( IValType ) [function, total, smtlib(pow1)] /* 2 ^Int (#width(T) -Int 1) */ - // ------------------------------------------------------------------------------------------------------ rule #pow1(i32) => 2147483648 rule #pow (i32) => 4294967296 rule #pow1(i64) => 9223372036854775808 @@ -317,25 +362,6 @@ The `#width` function returns the bit-width of a given `IValType`. // ---------------------- ``` -### Values - -Proper values are numbers annotated with their types. - -```k - syntax IVal ::= "<" IValType ">" Int [klabel(<_>_)] - syntax FVal ::= "<" FValType ">" Float [klabel(<_>_)] - syntax Val ::= "<" ValType ">" Number [klabel(<_>_)] - | IVal | FVal - // --------------------------- -``` - -We also add `undefined` as a value, which makes many partial functions in the semantics total. - -```k - syntax Val ::= "undefined" - // -------------------------- -``` - #### Value Operations The `#chop` function will ensure that an integer value is wrapped to the correct bit-width. @@ -377,10 +403,6 @@ These functions assume that the argument integer is in the valid range of signed Some operations extend integers from 1, 2, or 4 bytes, so a special function with a bit width argument helps with the conversion. ```k - syntax Int ::= #signed ( IValType , Int ) [function] - | #unsigned ( IValType , Int ) [function] - | #signedWidth ( Int , Int ) [function] - syntax Bool ::= definedSigned ( IValType, Int ) [function, total] | definedUnsigned( IValType, Int ) [function, total] @@ -434,9 +456,7 @@ WebAssembly is a stack-machine, so here we provide the stack to operate over. Operator `_++_` implements an append operator for sort `ValStack`. ```k - syntax ValStack ::= ".ValStack" [klabel(.ValStack), symbol] - | Val ":" ValStack [klabel(concatValStack), symbol] - | ValStack "++" ValStack [function, total] + syntax ValStack ::= ValStack "++" ValStack [function, total] // ----------------------------------------------------------------- rule .ValStack ++ VALSTACK' => VALSTACK' rule (SI : VALSTACK) ++ VALSTACK' => SI : (VALSTACK ++ VALSTACK') diff --git a/test.md b/test.md index 67bdcffcb..a13c9ab4a 100644 --- a/test.md +++ b/test.md @@ -12,10 +12,36 @@ Module `WASM-TEST-SYNTAX` is just used for program parsing and `WASM-TEST` consi ```k module WASM-TEST-SYNTAX - imports WASM-TEST + imports WASM-TEST-COMMON-SYNTAX imports WASM-TEXT-SYNTAX - imports WASM-AUXIL + imports WASM-INTERNAL-SYNTAX +endmodule + +module WASM-TEST-COMMON-SYNTAX + imports WASM-TEXT-COMMON-SYNTAX + imports WASM-DATA-INTERNAL-SYNTAX + imports WASM-AUXIL-SYNTAX imports WASM-REFERENCE-INTERPRETER-SYNTAX + + syntax Assertion ::= "#assertAndRemoveEqual" + | "#assertAndRemoveToken" + | "#assertTopStack" Val WasmString + | "#assertTopStackExactly" Val WasmString + | "#assertStack" ValStack WasmString + | "#assertLocal" Int Val WasmString + | "#assertGlobal" Index Val WasmString + | "#assertTrap" WasmString + | "#assertType" Int FuncType + | "#assertNextTypeIdx" Int + | "#assertFunction" Index FuncType VecType WasmString + | "#assertMemory" Index Int OptionalInt WasmString + | "#assertMemoryData" "(" Int "," Int ")" WasmString + | "#assertMemoryData" Int "(" Int "," Int ")" WasmString + | "#assertTable" Index Int OptionalInt WasmString + | "#assertTableElem" "(" Int "," Int ")" WasmString + | "#assertNamedModule" Identifier WasmString + | "#assertRegistrationUnnamed" WasmString WasmString + | "#assertRegistrationNamed" WasmString Identifier WasmString endmodule module WASM-REFERENCE-INTERPRETER-SYNTAX @@ -82,7 +108,7 @@ Here we inplement the conformance assertions specified in [spec interpreter] inc endmodule module WASM-TEST - imports WASM-REFERENCE-INTERPRETER-SYNTAX + imports WASM-TEST-COMMON-SYNTAX imports WASM-AUXIL imports WASM-TEXT ``` @@ -270,9 +296,6 @@ Except `assert_return` and `assert_trap`, the remaining rules are directly reduc And we implement some helper assertions to help testing. ```k - syntax Assertion ::= "#assertAndRemoveEqual" - | "#assertAndRemoveToken" - // -------------------------------------------- rule #assertAndRemoveEqual => #assertTopStack V .WasmString ~> ( drop ) ... V : VALSTACK => VALSTACK rule #assertAndRemoveToken => . ... @@ -284,8 +307,6 @@ And we implement some helper assertions to help testing. This asserts that a `trap` was just thrown. ```k - syntax Assertion ::= "#assertTrap" WasmString - // --------------------------------------------- rule trap ~> #assertTrap _ => . ... ``` @@ -294,10 +315,7 @@ This asserts that a `trap` was just thrown. These functions make assertions about the state of the `` cell. ```k - syntax Assertion ::= "#assertTopStack" Val WasmString - | "#assertTopStackExactly" Val WasmString - | "#assertStack" ValStack WasmString - | "#assertStackAux" ValStack ValStack + syntax Assertion ::= "#assertStackAux" ValStack ValStack // --------------------------------------------------------------- rule #assertTopStack S _ => . ... S : _VALSTACK rule #assertTopStack < ITYPE:IValType > VAL _ => . ... < ITYPE > VAL' : _VALSTACK @@ -320,9 +338,6 @@ These functions make assertions about the state of the `` cell. The operator `#assertLocal`/`#assertGlobal` operators perform a check for a local/global variable's value. ```k - syntax Assertion ::= "#assertLocal" Int Val WasmString - | "#assertGlobal" Index Val WasmString - // --------------------------------------------------------- rule #assertLocal INDEX VALUE _ => . ... ... INDEX |-> VALUE ... @@ -350,9 +365,6 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca `#assertNextTypeIdx` checks whether the number of types are allocated correctly. ```k - syntax Assertion ::= "#assertType" Int FuncType - | "#assertNextTypeIdx" Int - // --------------------------------------------- rule #assertType IDX FTYPE => . ... CUR @@ -375,7 +387,6 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca This simply checks that the given function exists in the `` cell and has the given signature and local types. ```k - syntax Assertion ::= "#assertFunction" Index FuncType VecType WasmString syntax Assertion ::= "#assertFunctionHelper" Int FuncType VecType // ------------------------------------------------------------------------ rule #assertFunction IDX FTYPE LTYPE _ => #assertFunctionHelper (FUNCADDRS {{ IDX }} orDefault -1) FTYPE LTYPE ... @@ -386,6 +397,7 @@ This simply checks that the given function exists in the `` cell and has ... requires isListIndex(IDX, FUNCADDRS) + rule #assertFunctionHelper ADDR FTYPE LTYPE => . ... @@ -403,8 +415,6 @@ This simply checks that the given function exists in the `` cell and has This asserts related operation about tables. ```k - syntax Assertion ::= "#assertTable" Index Int OptionalInt WasmString - // -------------------------------------------------------------------- rule #assertTable TFIDX SIZE MAX _MSG => . ... CUR @@ -423,8 +433,6 @@ This asserts related operation about tables. ... - syntax Assertion ::= "#assertTableElem" "(" Int "," Int ")" WasmString - // ---------------------------------------------------------------------- rule #assertTableElem (KEY , VAL) _MSG => . ... CUR @@ -447,8 +455,6 @@ This asserts related operation about tables. This checks that the last allocated memory has the given size and max value. ```k - syntax Assertion ::= "#assertMemory" Index Int OptionalInt WasmString - // --------------------------------------------------------------------- rule #assertMemory TFIDX SIZE MAX _MSG => . ... CUR @@ -467,9 +473,6 @@ This checks that the last allocated memory has the given size and max value. ... - syntax Assertion ::= "#assertMemoryData" "(" Int "," Int ")" WasmString - syntax Assertion ::= "#assertMemoryData" Int "(" Int "," Int ")" WasmString - // --------------------------------------------------------------------------- rule #assertMemoryData (KEY , VAL) MSG => #assertMemoryData CUR (KEY, VAL) MSG ... CUR @@ -496,8 +499,6 @@ These assertions test (and delete) module instances. These assertions act on the last module defined. ```k - syntax Assertion ::= "#assertNamedModule" Identifier WasmString - // --------------------------------------------------------------- rule [assertNamedModule]: #assertNamedModule NAME _S => . ... ... NAME |-> IDX ... @@ -518,9 +519,6 @@ Registry Assertations We also want to be able to test that the embedder's registration function is working. ```k - syntax Assertion ::= "#assertRegistrationUnnamed" WasmString WasmString - | "#assertRegistrationNamed" WasmString Identifier WasmString - // ---------------------------------------------------------------------------------- rule #assertRegistrationUnnamed REGNAME _ => . ... IDX ... REGNAME |-> IDX ... diff --git a/tests/proofs/simple-arithmetic-spec.k b/tests/proofs/simple-arithmetic-spec.k index 0c2ad2fef..03665d8f1 100644 --- a/tests/proofs/simple-arithmetic-spec.k +++ b/tests/proofs/simple-arithmetic-spec.k @@ -15,4 +15,18 @@ module SIMPLE-ARITHMETIC-SPEC S:ValStack => < ITYPE > (X +Int Y) : S requires 0 <=Int X andBool 0 <=Int Y andBool (X +Int Y) i32.const #unsigned(i32, #signed(i32, #pow(i32) -Int 1)) + => . ... + + S => < i32 > #pow(i32) -Int 1 : S + + + // #unsigned( i64 , #signed( i64 , 2^64 - 1 ) ) == 2^64 - 1 + claim i64.const #unsigned(i64, #signed(i64, #pow(i64) -Int 1)) + => . ... + + S => < i64 > #pow(i64) -Int 1 : S + endmodule diff --git a/tests/simple/arithmetic.wast b/tests/simple/arithmetic.wast index e51fd81f3..7defa8eae 100644 --- a/tests/simple/arithmetic.wast +++ b/tests/simple/arithmetic.wast @@ -59,7 +59,7 @@ #assertTrap "i32.div_s 3" (i32.const #pow1(i32)) -(i32.const #pow(i32) -Int 1) +(i32.sub (i32.const #pow(i32)) (i32.const 1)) (i32.div_s) #assertTrap "i32.div_s 4" @@ -89,7 +89,7 @@ #assertTrap "rem_s" (i32.const #pow1(i32)) -(i32.const #pow(i32) -Int 1) +(i32.sub (i32.const #pow(i32)) (i32.const 1)) (i32.rem_s) #assertTopStack 0 "rem_s edge case" diff --git a/tests/simple/bitwise.wast b/tests/simple/bitwise.wast index 0791e6676..dd0adbfd0 100644 --- a/tests/simple/bitwise.wast +++ b/tests/simple/bitwise.wast @@ -19,39 +19,39 @@ #assertTopStack < i32 > 4 "shl 1" (i32.const 2) -(i32.const #pow1(i32) +Int 1) +(i32.add (i32.const #pow1(i32)) (i32.const 1)) (i32.shl) #assertTopStack < i32 > 4 "shl 2" (i32.const #pow1(i32)) (i32.const 2) (i32.shr_u) -#assertTopStack < i32 > 2 ^Int 29 "shr_u 1" +#assertTopStack < i32 > 536870912 "shr_u 1" ;; 2 ^Int 29 (i32.const 2) (i32.const 2) (i32.shr_u) #assertTopStack < i32 > 0 "shr_u 2" -(i32.const #pow(i32) -Int 2) +(i32.sub (i32.const #pow(i32)) (i32.const 2)) (i32.const 1) (i32.shr_s) -#assertTopStack < i32 > #pow(i32) -Int 1 "shr_s 1" +#assertTopStack < i32 > 4294967295 "shr_s 1" ;; #pow(i32) -Int 1 (i32.const 2) (i32.const 2) (i32.shr_s) #assertTopStack < i32 > 0 "shr_s 2" -(i32.const #pow1(i32) +Int 2) +(i32.add (i32.const #pow1(i32)) (i32.const 2)) (i32.const 3) (i32.rotl) #assertTopStack < i32 > 20 "rotl" -(i32.const #pow1(i32) +Int 16) +(i32.add (i32.const #pow1(i32)) (i32.const 16)) (i32.const 3) (i32.rotr) -#assertTopStack < i32 > 2 ^Int 28 +Int 2 "rotr" +#assertTopStack < i32 > 268435458 "rotr" ;; 2 ^Int 28 +Int 2 ;; clz @@ -76,17 +76,19 @@ (i64.clz) #assertTopStack < i64 > 63 "clz 1" -(i32.const 2 ^Int 32 -Int 1) +(i32.sub (i32.const #pow(i32)) (i32.const 1)) (i32.clz) #assertTopStack < i32 > 0 "clz 2^32 - 1" -(i64.const 2 ^Int 64 -Int 1) + +(i64.sub (i64.const #pow(i64)) (i64.const 1)) (i64.clz) #assertTopStack < i64 > 0 "clz 2^64 - 1" -(i32.const 2 ^Int 31 -Int 1) +(i32.sub (i32.const #pow1(i32)) (i32.const 1)) (i32.clz) #assertTopStack < i32 > 1 "clz 2^31 - 1" -(i64.const 2 ^Int 63 -Int 1) + +(i64.sub (i64.const #pow1(i64)) (i64.const 1)) (i64.clz) #assertTopStack < i64 > 1 "clz 2^63 - 1" @@ -112,10 +114,10 @@ (i64.ctz) #assertTopStack < i64 > 0 "ctz 1" -(i32.const 2 ^Int 32 -Int 1) +(i32.sub (i32.const #pow(i32)) (i32.const 1)) (i32.ctz) #assertTopStack < i32 > 0 "ctz 2^32 - 1" -(i64.const 2 ^Int 64 -Int 1) +(i64.sub (i64.const #pow(i64)) (i64.const 1)) (i64.ctz) #assertTopStack < i64 > 0 "ctz 2^64 - 1" @@ -142,10 +144,10 @@ (i64.popcnt) #assertTopStack < i64 > 1 "popcnt 1" -(i32.const 2 ^Int 32 -Int 1) +(i32.sub (i32.const #pow(i32)) (i32.const 1)) (i32.popcnt) #assertTopStack < i32 > 32 "popcnt 2^32 - 1" -(i64.const 2 ^Int 64 -Int 1) +(i64.sub (i64.const #pow(i64)) (i64.const 1)) (i64.popcnt) #assertTopStack < i64 > 64 "popcnt 2^64 - 1" diff --git a/tests/simple/comparison.wast b/tests/simple/comparison.wast index ae7f0f441..bd06f5925 100644 --- a/tests/simple/comparison.wast +++ b/tests/simple/comparison.wast @@ -42,8 +42,8 @@ (i32.gt_u) #assertTopStack < i32 > 0 "gt_u" -(i32.const #pow1(i32) +Int 7) -(i32.const #pow1(i32) +Int 15) +(i32.add (i32.const #pow1(i32)) (i32.const 7)) +(i32.add (i32.const #pow1(i32)) (i32.const 15)) (i32.lt_s) #assertTopStack < i32 > 1 "lt_s 1" @@ -52,8 +52,8 @@ (i32.lt_s) #assertTopStack < i32 > 1 "lt_s 2" -(i32.const #pow1(i32) +Int 7) -(i32.const #pow1(i32) +Int 15) +(i32.add (i32.const #pow1(i32)) (i32.const 7)) +(i32.add (i32.const #pow1(i32)) (i32.const 15)) (i32.gt_s) #assertTopStack < i32 > 0 "gt_s 1" @@ -82,8 +82,8 @@ (i32.ge_u) #assertTopStack < i32 > 1 "ge_u 2" -(i32.const #pow1(i32) +Int 7) -(i32.const #pow1(i32) +Int 15) +(i32.add (i32.const #pow1(i32)) (i32.const 7)) +(i32.add (i32.const #pow1(i32)) (i32.const 15)) (i32.le_s) #assertTopStack < i32 > 1 "le_s 1" @@ -97,8 +97,8 @@ (i32.le_s) #assertTopStack < i32 > 1 "le_s 3" -(i32.const #pow1(i32) +Int 7) -(i32.const #pow1(i32) +Int 15) +(i32.add (i32.const #pow1(i32)) (i32.const 7)) +(i32.add (i32.const #pow1(i32)) (i32.const 15)) (i32.ge_s) #assertTopStack < i32 > 0 "ge_s 1" diff --git a/tests/simple/constants.wast b/tests/simple/constants.wast index f221feda1..572683376 100644 --- a/tests/simple/constants.wast +++ b/tests/simple/constants.wast @@ -11,9 +11,9 @@ #assertTopStack < i64 > 71 "i64" (i32.const #unsigned(i32, -5)) -#assertTopStack < i32 > #pow(i32) -Int 5 "i32 manual unsigned" +#assertTopStack < i32 > 4294967291 "i32 manual unsigned" ;; #pow(i32) -Int 5 -(i32.const #pow(i32) -Int 5) +(i32.sub (i32.const #pow(i32)) (i32.const 5)) #assertTopStack < i32 > -5 "i32 manual unsigned" (i32.const -5) @@ -22,14 +22,14 @@ (i32.const #unsigned(i32, -5)) #assertTopStack < i32 > -5 "i32 signed assert" -(i32.const #pow(i32) +Int 1) +(i32.add (i32.const #pow(i32)) (i32.const 1)) #assertTopStack < i32 > 1 "i32 overflow" (i32.const -1) -#assertTopStackExactly < i32 > #pow(i32) -Int 1 "i32 overflow" +#assertTopStackExactly < i32 > 4294967295 "i32 overflow" (i64.const -1) -#assertTopStackExactly < i64 > #pow(i64) -Int 1 "i62 overflow" +#assertTopStackExactly < i64 > 18446744073709551615 "i62 overflow" ;; #pow(i64) -Int 1 ;; Floating point ;; -------------- @@ -63,16 +63,10 @@ (i32.const #unsigned(i32, #signed(i32, #pow1(i32)))) #assertTopStack < i32 > #pow1(i32) "#unsigned . #signed 2" -(i32.const #unsigned(i32, #signed(i32, #pow(i32) -Int 1))) -#assertTopStack < i32 > #pow(i32) -Int 1 "#unsigned . #signed 3" - (i64.const #unsigned(i64, #signed(i64, 0))) #assertTopStack < i64 > 0 "#unsigned . #signed 4" (i64.const #unsigned(i64, #signed(i64, #pow1(i64)))) #assertTopStack < i64 > #pow1(i64) "#unsigned . #signed 5" -(i64.const #unsigned(i64, #signed(i64, #pow(i64) -Int 1))) -#assertTopStack < i64 > #pow(i64) -Int 1 "#unsigned . #signed 6" - #clearConfig diff --git a/tests/simple/memory.wast b/tests/simple/memory.wast index 5610f5ca3..87193865d 100644 --- a/tests/simple/memory.wast +++ b/tests/simple/memory.wast @@ -69,7 +69,7 @@ (i64.store16 offset=2) #assertMemoryData (3, 1) "store16" (i32.const 1) -(i64.const #pow(i32) +Int 1) +(i64.add (i64.const #pow(i32)) (i64.const 1)) (i64.store16 offset=2) #assertMemoryData (3, 1) "store32" #assertMemory 0 1 .Int "" @@ -100,7 +100,7 @@ (memory 1) (i32.const 15) -(i64.const #pow(i32) -Int 1) +(i64.sub (i64.const #pow(i32)) (i64.const 1)) (i64.store) (i32.const 15) (i32.load8_u) @@ -116,7 +116,7 @@ #assertTopStack -1 "load16 signed" (i32.const 15) (i64.load32_u ) -#assertTopStack #pow(i32) -Int 1 "load32 unsigned1" +#assertTopStack 4294967295 "load32 unsigned1" ;; #pow(i32) -Int 1 (i32.const 15) (i64.load32_s ) #assertTopStack -1 "load32 signed1" @@ -138,7 +138,7 @@ (memory 1) (i32.const 1) -(i64.const #pow(i64) -Int 1) +(i64.sub (i64.const #pow(i64)) (i64.const 1)) (i64.store) (i32.const 5) (i32.const 0) (i32.store ) @@ -153,7 +153,7 @@ #clearConfig (memory 1) -(i32.const 1) (i64.const #pow(i64) -Int 1) +(i32.const 1) (i64.sub (i64.const #pow(i64)) (i64.const 1)) (i64.store ) (i32.const 2) (i32.const 0) (i32.store8 ) diff --git a/wasm-text.md b/wasm-text.md index 6d2299aed..a5da10d6b 100644 --- a/wasm-text.md +++ b/wasm-text.md @@ -6,7 +6,6 @@ require "wasm.md" require "data.md" module WASM-TEXT-SYNTAX - imports WASM-TEXT imports WASM-SYNTAX imports WASM-TOKEN-SYNTAX endmodule diff --git a/wasm.md b/wasm.md index 24213b4b6..39adb9e74 100644 --- a/wasm.md +++ b/wasm.md @@ -22,7 +22,7 @@ Common Syntax ```k module WASM-COMMON-SYNTAX imports WASM-DATA-COMMON-SYNTAX - imports WASM-NUMERIC + imports WASM-NUMERIC-SYNTAX ``` ### Text Format @@ -156,6 +156,26 @@ The following are kept abstract, and can be extended in other formats, such as t endmodule ``` +Internal Syntax +--------------- + +```k +module WASM-INTERNAL-SYNTAX + imports WASM-DATA-INTERNAL-SYNTAX + + syntax Instr ::= "init_local" Int Val + | "init_locals" ValStack + | "#init_locals" Int ValStack + // -------------------------------------------- + + syntax Int ::= #pageSize() [function, total] + syntax Int ::= #maxMemorySize() [function, total] + syntax Int ::= #maxTableSize() [function, total] + // ------------------------------------------ + +endmodule +``` + Semantics --------- @@ -166,6 +186,7 @@ module WASM imports MAP-INT-TO-INT imports MAP-INT-TO-INT-PRIMITIVE imports WASM-COMMON-SYNTAX + imports WASM-INTERNAL-SYNTAX imports WASM-DATA imports WASM-DATA-TOOLS imports WASM-NUMERIC @@ -511,10 +532,6 @@ Variable Operators The various `init_local` variants assist in setting up the `locals` cell. ```k - syntax Instr ::= "init_local" Int Val - | "init_locals" ValStack - | "#init_locals" Int ValStack - // -------------------------------------------- rule init_local INDEX VALUE => . ... LOCALS => LOCALS [ INDEX <- VALUE ] @@ -1137,10 +1154,6 @@ Incidentally, the page size is 2^16 bytes. The maximum of table size is 2^32 bytes. ```k - syntax Int ::= #pageSize() [function, total] - syntax Int ::= #maxMemorySize() [function, total] - syntax Int ::= #maxTableSize() [function, total] - // ------------------------------------------ rule #pageSize() => 65536 rule #maxMemorySize() => 65536 rule #maxTableSize() => 4294967296