@@ -129,7 +129,7 @@ Passing Control
129
129
The test embedder passes control to the execution cell in Wasm.
130
130
131
131
``` k
132
- rule <k> PGM => . </k>
132
+ rule <k> PGM => .K </k>
133
133
<instrs> .K
134
134
=> #initSpectestModule
135
135
~> sequenceStmts(text2abstract(PGM))
@@ -165,7 +165,7 @@ We add `token` as a value in order to use as a separator in `<valstack>`.
165
165
``` k
166
166
syntax Val ::= "token"
167
167
// ----------------------
168
- rule <instrs> token => . ... </instrs>
168
+ rule <instrs> token => .K ... </instrs>
169
169
<valstack> S => token : S </valstack>
170
170
171
171
syntax ValStack ::= takeUntilToken(ValStack) [function, total]
@@ -183,7 +183,7 @@ We add `token` as a value in order to use as a separator in `<valstack>`.
183
183
184
184
syntax Assertion ::= "#dropUntilToken"
185
185
// --------------------------------------------------
186
- rule <instrs> #dropUntilToken => . ... </instrs>
186
+ rule <instrs> #dropUntilToken => .K ... </instrs>
187
187
<valstack> S => dropUntilToken(S) </valstack>
188
188
```
189
189
@@ -255,7 +255,7 @@ We will reference modules by name in imports.
255
255
rule <instrs> ( register S ID:Identifier ) => ( register S IDX ) ... </instrs>
256
256
<moduleIds> ... ID |-> IDX ... </moduleIds>
257
257
258
- rule <instrs> ( register S:WasmString IDX:Int ) => . ... </instrs>
258
+ rule <instrs> ( register S:WasmString IDX:Int ) => .K ... </instrs>
259
259
<moduleRegistry> ... .Map => S |-> IDX ... </moduleRegistry>
260
260
```
261
261
@@ -363,13 +363,13 @@ Except `assert_return` and `assert_trap`, the remaining rules are directly reduc
363
363
...
364
364
</instrs>
365
365
366
- rule <instrs> (assert_return_canonical_nan _ACT) => . ... </instrs>
367
- rule <instrs> (assert_return_arithmetic_nan _ACT) => . ... </instrs>
366
+ rule <instrs> (assert_return_canonical_nan _ACT) => .K ... </instrs>
367
+ rule <instrs> (assert_return_arithmetic_nan _ACT) => .K ... </instrs>
368
368
rule <instrs> (assert_trap ACT:Action DESC) => ACT ~> #assertTrap DESC ... </instrs>
369
- rule <instrs> (assert_exhaustion _ACT:Action _DESC) => . ... </instrs>
370
- rule <instrs> (assert_malformed _MOD _DESC) => . ... </instrs>
371
- rule <instrs> (assert_invalid _MOD _DESC) => . ... </instrs>
372
- rule <instrs> (assert_unlinkable _MOD _DESC) => . ... </instrs>
369
+ rule <instrs> (assert_exhaustion _ACT:Action _DESC) => .K ... </instrs>
370
+ rule <instrs> (assert_malformed _MOD _DESC) => .K ... </instrs>
371
+ rule <instrs> (assert_invalid _MOD _DESC) => .K ... </instrs>
372
+ rule <instrs> (assert_unlinkable _MOD _DESC) => .K ... </instrs>
373
373
rule <instrs> (assert_trap MOD:ModuleDecl DESC) => sequenceStmts(text2abstract(MOD .Stmts)) ~> #assertTrap DESC ... </instrs>
374
374
```
375
375
@@ -390,7 +390,7 @@ And we implement some helper assertions to help testing.
390
390
This asserts that a ` trap ` was just thrown.
391
391
392
392
``` k
393
- rule <instrs> trap ~> #assertTrap _ => . ... </instrs>
393
+ rule <instrs> trap ~> #assertTrap _ => .K ... </instrs>
394
394
```
395
395
396
396
### ValStack Assertions
@@ -400,16 +400,16 @@ These functions make assertions about the state of the `<valstack>` cell.
400
400
``` k
401
401
syntax Assertion ::= "#assertStackAux" ValStack ValStack
402
402
// ---------------------------------------------------------------
403
- rule <instrs> #assertTopStack VAL _ => . ... </instrs>
403
+ rule <instrs> #assertTopStack VAL _ => .K ... </instrs>
404
404
<valstack> VAL' : _ </valstack>
405
405
requires equalVal(VAL, VAL')
406
406
407
- rule <instrs> #assertTopStackExactly A _ => . ... </instrs> <valstack> A : _VALSTACK </valstack>
407
+ rule <instrs> #assertTopStackExactly A _ => .K ... </instrs> <valstack> A : _VALSTACK </valstack>
408
408
409
409
rule <instrs> #assertStack S1 _ => #assertStackAux S1 S2 ... </instrs>
410
410
<valstack> S2 </valstack>
411
411
412
- rule <instrs> #assertStackAux .ValStack _ => . ... </instrs>
412
+ rule <instrs> #assertStackAux .ValStack _ => .K ... </instrs>
413
413
rule <instrs> #assertStackAux (V1 : S1) (V2 : S2) => #assertStackAux S1 S2 ... </instrs>
414
414
requires equalVal(V1, V2)
415
415
@@ -427,10 +427,10 @@ These functions make assertions about the state of the `<valstack>` cell.
427
427
The operator ` #assertLocal ` /` #assertGlobal ` operators perform a check for a local/global variable's value.
428
428
429
429
``` k
430
- rule <instrs> #assertLocal INDEX VALUE _ => . ... </instrs>
430
+ rule <instrs> #assertLocal INDEX VALUE _ => .K ... </instrs>
431
431
<locals> ... INDEX |-> VALUE ... </locals>
432
432
433
- rule <instrs> #assertGlobal TFIDX VALUE _ => . ... </instrs>
433
+ rule <instrs> #assertGlobal TFIDX VALUE _ => .K ... </instrs>
434
434
<curModIdx> CUR </curModIdx>
435
435
<moduleInst>
436
436
<modIdx> CUR </modIdx>
@@ -454,15 +454,15 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca
454
454
` #assertNextTypeIdx ` checks whether the number of types are allocated correctly.
455
455
456
456
``` k
457
- rule <instrs> #assertType IDX FTYPE => . ... </instrs>
457
+ rule <instrs> #assertType IDX FTYPE => .K ... </instrs>
458
458
<curModIdx> CUR </curModIdx>
459
459
<moduleInst>
460
460
<modIdx> CUR </modIdx>
461
461
<types> ... IDX |-> FTYPE ... </types>
462
462
...
463
463
</moduleInst>
464
464
465
- rule <instrs> #assertNextTypeIdx IDX => . ... </instrs>
465
+ rule <instrs> #assertNextTypeIdx IDX => .K ... </instrs>
466
466
<curModIdx> CUR </curModIdx>
467
467
<moduleInst>
468
468
<modIdx> CUR </modIdx>
@@ -487,7 +487,7 @@ This simply checks that the given function exists in the `<funcs>` cell and has
487
487
</moduleInst>
488
488
requires isListIndex(IDX, FUNCADDRS)
489
489
490
- rule <instrs> #assertFunctionHelper ADDR FTYPE LTYPE => . ... </instrs>
490
+ rule <instrs> #assertFunctionHelper ADDR FTYPE LTYPE => .K ... </instrs>
491
491
<funcs>
492
492
<funcDef>
493
493
<fAddr> ADDR </fAddr>
@@ -504,7 +504,7 @@ This simply checks that the given function exists in the `<funcs>` cell and has
504
504
This asserts related operation about tables.
505
505
506
506
``` k
507
- rule <instrs> #assertTable TFIDX SIZE MAX _MSG => . ... </instrs>
507
+ rule <instrs> #assertTable TFIDX SIZE MAX _MSG => .K ... </instrs>
508
508
<curModIdx> CUR </curModIdx>
509
509
<moduleInst>
510
510
<modIdx> CUR </modIdx>
@@ -523,7 +523,7 @@ This asserts related operation about tables.
523
523
</tabs>
524
524
requires size(DATA) ==Int SIZE
525
525
526
- rule <instrs> #assertTableElem (KEY , VAL:Int) _MSG => . ... </instrs>
526
+ rule <instrs> #assertTableElem (KEY , VAL:Int) _MSG => .K ... </instrs>
527
527
<curModIdx> CUR </curModIdx>
528
528
<moduleInst>
529
529
<modIdx> CUR </modIdx>
@@ -562,7 +562,7 @@ This asserts related operation about tables.
562
562
This checks that the last allocated memory has the given size and max value.
563
563
564
564
``` k
565
- rule <instrs> #assertMemory TFIDX SIZE MAX _MSG => . ... </instrs>
565
+ rule <instrs> #assertMemory TFIDX SIZE MAX _MSG => .K ... </instrs>
566
566
<curModIdx> CUR </curModIdx>
567
567
<moduleInst>
568
568
<modIdx> CUR </modIdx>
@@ -583,7 +583,7 @@ This checks that the last allocated memory has the given size and max value.
583
583
rule <instrs> #assertMemoryData (KEY , VAL) MSG => #assertMemoryData CUR (KEY, VAL) MSG ... </instrs>
584
584
<curModIdx> CUR </curModIdx>
585
585
586
- rule <instrs> #assertMemoryData MODIDX (KEY , VAL) _MSG => . ... </instrs>
586
+ rule <instrs> #assertMemoryData MODIDX (KEY , VAL) _MSG => .K ... </instrs>
587
587
<moduleInst>
588
588
<modIdx> MODIDX </modIdx>
589
589
<memAddrs> wrap(0) Int2Int|-> wrap(ADDR) </memAddrs>
@@ -607,7 +607,7 @@ These assertions act on the last module defined.
607
607
608
608
``` k
609
609
rule [assertNamedModule]:
610
- <instrs> #assertNamedModule NAME _S => . ... </instrs>
610
+ <instrs> #assertNamedModule NAME _S => .K ... </instrs>
611
611
<moduleIds> ... NAME |-> IDX ... </moduleIds>
612
612
<moduleInstances>
613
613
<moduleInst>
@@ -626,11 +626,11 @@ Registry Assertations
626
626
We also want to be able to test that the embedder's registration function is working.
627
627
628
628
``` k
629
- rule <instrs> #assertRegistrationUnnamed REGNAME _ => . ... </instrs>
629
+ rule <instrs> #assertRegistrationUnnamed REGNAME _ => .K ... </instrs>
630
630
<modIdx> IDX </modIdx>
631
631
<moduleRegistry> ... REGNAME |-> IDX ... </moduleRegistry>
632
632
633
- rule <instrs> #assertRegistrationNamed REGNAME _NAME _ => . ... </instrs>
633
+ rule <instrs> #assertRegistrationNamed REGNAME _NAME _ => .K ... </instrs>
634
634
<modIdx> IDX </modIdx>
635
635
<moduleRegistry> ... REGNAME |-> IDX ... </moduleRegistry>
636
636
```
0 commit comments