diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md index 2cd20e5f1..2374dcf8c 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md @@ -34,8 +34,7 @@ module WASM-AUXIL _ => .Bag _ => 0 _ => .Bag - _ => 0 - _ => .Bag + _ => .List _ => 0 _ => .Bag _ => 0 diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md index 55e91d37b..a83d11f14 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md @@ -570,18 +570,12 @@ This checks that the last allocated memory has the given size and max value. CUR IDS - #ContextLookup(IDS, TFIDX) |-> ADDR + ListItem(ADDR) ... - - - ADDR - MAX - SIZE - ... - - ... - + MEMS + requires ADDR #assertMemoryData (KEY , VAL) MSG => #assertMemoryData CUR (KEY, VAL) MSG ... CUR @@ -589,18 +583,12 @@ This checks that the last allocated memory has the given size and max value. rule #assertMemoryData MODIDX (KEY , VAL) _MSG => .K ... MODIDX - 0 |-> ADDR + ListItem(ADDR) ... - - - ADDR - BM - ... - - ... - - requires #getRange(BM, KEY, 1) ==Int VAL + MEMS + requires ADDR .Map 0 .Map - .Map + .List .Map .Map 0 @@ -257,15 +257,7 @@ module WASM 0 - - - 0 - .Int - 0 - .SparseBytes - - - 0 + .List 0 @@ -1352,7 +1344,8 @@ The importing and exporting parts of specifications are dealt with in the respec ```k syntax MemoryDefn ::= #memory(limits: Limits, metadata: OptionalId) [symbol(aMemoryDefn)] syntax Alloc ::= allocmemory (OptionalId, Int, OptionalInt) - // ----------------------------------------------------------- + syntax KItem ::= memInst(mmax: OptionalInt, msize: Int, mdata: SparseBytes) + // --------------------------------------------------------------------------- rule #memory(... limits: #limitsMin(MIN), metadata: OID) => allocmemory(OID, MIN, .Int) ... requires MIN <=Int #maxMemorySize() rule #memory(... limits: #limits(MIN, MAX), metadata: OID) => allocmemory(OID, MIN, MAX) ... @@ -1364,21 +1357,10 @@ The importing and exporting parts of specifications are dealt with in the respec CUR IDS => #saveId(IDS, ID, 0) - .Map => (0 |-> NEXTADDR) + .List => ListItem(size(MEMS)) ... - NEXTADDR => NEXTADDR +Int 1 - - ( .Bag - => - NEXTADDR - MAX - MIN - ... - - ) - ... - + MEMS => MEMS ListItem(memInst(MAX, MIN, .SparseBytes)) ``` The assorted store operations take an address of type `i32` and a value. @@ -1396,36 +1378,27 @@ The value is encoded as bytes and stored at the "effective address", which is th rule #store(ITYPE:IValType, SOP, OFFSET) => ITYPE . SOP (IDX +Int OFFSET) VAL ... < ITYPE > VAL : < i32 > IDX : VALSTACK => VALSTACK - rule store { WIDTH EA VAL } => store { WIDTH EA VAL ({MEMADDRS[0] orDefault 0}:>Int) } ... + rule store { WIDTH EA VAL } => store { WIDTH EA VAL ADDR } ... CUR CUR - MEMADDRS + ListItem(ADDR) ... - requires 0 in_keys(MEMADDRS) andBool size(MEMADDRS) ==Int 1 andBool isInt(MEMADDRS[0] orDefault 0) - [preserves-definedness] rule store { WIDTH EA VAL ADDR } => .K ... - - ADDR - SIZE - DATA => #setRange(DATA, EA, VAL, #numBytes(WIDTH)) - ... - - requires (EA +Int #numBytes(WIDTH)) <=Int (SIZE *Int #pageSize()) + MEMS => MEMS [ ADDR <- #let memInst(MAX, SIZE, DATA) = MEMS[ADDR] #in memInst(MAX, SIZE, #setRange(DATA, EA, VAL, #numBytes(WIDTH))) ] + requires ADDR store { WIDTH EA _ ADDR } => trap ... - - ADDR - SIZE - ... - - requires (EA +Int #numBytes(WIDTH)) >Int (SIZE *Int #pageSize()) + MEMS + requires ADDR Int (msize(MEMS[ADDR]) *Int #pageSize()) rule ITYPE . store EA VAL => store { ITYPE EA VAL } ... rule _ . store8 EA VAL => store { i8 EA #wrap(1, VAL) } ... @@ -1457,32 +1430,23 @@ Sort `Signedness` is defined in module `BYTES`. rule ITYPE . load16_s EA:Int => load { ITYPE i16 EA Signed } ... rule i64 . load32_s EA:Int => load { i64 i32 EA Signed } ... - rule load { ITYPE WIDTH EA SIGN } => load { ITYPE WIDTH EA SIGN ({MEMADDRS[0] orDefault 0}:>Int)} ... + rule load { ITYPE WIDTH EA SIGN } => load { ITYPE WIDTH EA SIGN ADDR:Int } ... CUR CUR - MEMADDRS + ListItem(ADDR) ... - requires 0 in_keys(MEMADDRS) andBool size(MEMADDRS) ==Int 1 andBool isInt(MEMADDRS[0] orDefault 0) - [preserves-definedness] - rule load { ITYPE WIDTH EA SIGN ADDR:Int} => load { ITYPE WIDTH EA SIGN DATA } ... - - ADDR - SIZE - DATA - ... - - requires (EA +Int #numBytes(WIDTH)) <=Int (SIZE *Int #pageSize()) + rule load { ITYPE WIDTH EA SIGN ADDR:Int} => load { ITYPE WIDTH EA SIGN mdata(MEMS[ADDR]) } ... + MEMS + requires ADDR load { _ WIDTH EA _ ADDR:Int} => trap ... - - ADDR - SIZE - ... - - requires (EA +Int #numBytes(WIDTH)) >Int (SIZE *Int #pageSize()) + MEMS + requires ADDR Int (msize(MEMS[ADDR]) *Int #pageSize()) rule load { ITYPE WIDTH EA Signed DATA:SparseBytes } => #chop(< ITYPE > #signed(WIDTH, #getRange(DATA, EA, #numBytes(WIDTH)))) ... [preserves-definedness] @@ -1497,18 +1461,15 @@ The `size` operation returns the size of the memory, measured in pages. [Memory Size](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-size) ```k - rule memory.size => < i32 > SIZE ... + rule memory.size => < i32 > msize(MEMS[ADDR]) ... CUR CUR - 0 |-> ADDR + ListItem(ADDR) ... - - ADDR - SIZE - ... - + MEMS + requires ADDR ` field in the configuration to `true rule memory.grow => grow N ... < i32 > N : VALSTACK => VALSTACK - rule grow N => < i32 > SIZE ... + rule grow N => < i32 > msize(MEMS[ADDR]) ... CUR CUR - 0 |-> ADDR + ListItem(ADDR) ... - - ADDR - MAX - SIZE => SIZE +Int N - ... - - requires #growthAllowed(SIZE +Int N, MAX) + MEMS => #let memInst(MAX, SIZE, DATA) = MEMS[ADDR] #in MEMS[ADDR <- memInst(MAX, SIZE +Int N, DATA)] + requires ADDR grow N => < i32 > #unsigned(i32, -1) ... DET:Bool CUR CUR - 0 |-> ADDR + ListItem(ADDR) ... - - ADDR - MAX - SIZE - ... - - requires notBool DET - orBool notBool #growthAllowed(SIZE +Int N, MAX) + MEMS + requires ADDR CUR CUR - 0 |-> ADDR + ListItem(ADDR) ... - - ADDR - SIZE - ... - - requires N +Int D >Int SIZE *Int #pageSize() + MEMS + requires ADDR Int SIZE *Int #pageSize()) rule fillTrap N VAL D => fill N VAL D ... [owise] @@ -1607,15 +1557,11 @@ The spec states that this is really a sequence of `i32.store8` instructions, but CUR CUR - 0 |-> ADDR + ListItem(ADDR) ... - - ADDR - DATA => replaceAt(DATA, D, padRightBytes(.Bytes, N, VAL)) - ... - - requires notBool N ==Int 0 + MEMS => MEMS [ ADDR <- #let memInst(MAX, SIZE, DATA) = MEMS[ADDR] #in memInst(MAX, SIZE, replaceAt(DATA, D, padRightBytes(.Bytes, N, VAL))) ] + requires ADDR CUR CUR - 0 |-> ADDR + ListItem(ADDR) ... - - ADDR - SIZE - ... - - requires D +Int N >Int SIZE *Int #pageSize() - orBool S +Int N >Int SIZE *Int #pageSize() + MEMS + requires ADDR Int SIZE *Int #pageSize() + orBool S +Int N >Int SIZE *Int #pageSize()) rule copyTrap N S D => copy N S D ... [owise] @@ -1654,15 +1597,11 @@ performing a series of load and store operations as stated in the spec. CUR CUR - 0 |-> ADDR + ListItem(ADDR) ... - - ADDR - DATA => replaceAt(DATA, D, #getBytesRange(DATA, S, N)) - ... - - requires notBool N ==Int 0 + MEMS => MEMS [ ADDR <- #let memInst(MAX, SIZE, DATA) = MEMS[ADDR] #in memInst(MAX, SIZE, replaceAt(DATA, D, #getBytesRange(DATA, S, N))) ] + requires ADDR #data(IDX, IS, DATA) => sequenceInstrs(IS) ~> data { IDX DATA } ... - rule data { MEMIDX DSBYTES } => trap ... + rule data { 0 DSBYTES } => trap ... < i32 > OFFSET : _STACK CUR CUR - MEMIDX |-> ADDR + ListItem(ADDR) ... + MEMS ADDR SIZE ... - requires OFFSET +Int lengthBytes(DSBYTES) >Int SIZE *Int #pageSize() + requires ADDR Int SIZE *Int #pageSize()) // For now, deal only with memory 0. - rule data { MEMIDX DSBYTES } => .K ... + rule data { 0 DSBYTES } => .K ... < i32 > OFFSET : STACK => STACK CUR CUR - MEMIDX |-> ADDR + ListItem(ADDR) ... @@ -1778,6 +1719,8 @@ The `data` initializer simply puts these bytes into the specified memory, starti DATA => #setRange(DATA, OFFSET, Bytes2Int(DSBYTES, LE, Unsigned), lengthBytes(DSBYTES)) ... + MEMS => #let memInst(MAX, SIZE, DATA) = MEMS[ADDR] #in MEMS [ ADDR <- memInst(MAX, SIZE, #setRange(DATA, OFFSET, Bytes2Int(DSBYTES, LE, Unsigned), lengthBytes(DSBYTES))) ] + requires ADDR CUR IDS => #saveId(IDS, OID, 0) - .Map => 0 |-> ADDR + .List => ListItem(ADDRS[#ContextLookup(IDS', TFIDX)]) ... ... MOD |-> MODIDX ... MODIDX IDS' - ... #ContextLookup(IDS' , TFIDX) |-> ADDR ... + ADDRS ... NAME |-> TFIDX ... ... - - ADDR - MAX - SIZE - ... - - requires #limitsMatchImport(SIZE, MAX, LIM) + MEMS + requires #ContextLookup(IDS', TFIDX) Int Int] #in #limitsMatchImport(SIZE, MAX, LIM)) rule #import(MOD, NAME, #globalDesc(... id: OID, type: MUT TYP) ) => .K ... CUR diff --git a/tests/success-llvm.out b/tests/success-llvm.out index bdfd25dfa..2dee704ab 100644 --- a/tests/success-llvm.out +++ b/tests/success-llvm.out @@ -43,11 +43,8 @@ 0 - .MemInstCellMap + .List - - 0 - .GlobalInstCellMap