search

Wasm-DSL / spectec

Wasm SpecTec specification tools
https://wasm-dsl.github.io/spectec/
Other
27 stars 9 forks source link

Add consttype #78

Closed ShinWonho closed 8 months ago

ShinWonho commented 8 months ago

I added consttype to merge the num case and the vec case in array.init_data and array.new_data, because prose is not properly generated without merging them.

rule Step_read/array.init_data-num:
  z; (REF.ARRAY_ADDR a) (CONST I32 i) (CONST I32 j) (CONST I32 n) (ARRAY.INIT_DATA x y)  ~> ...
  -- otherwise
  -- Expand: $type(z, x) ~~ ARRAY (mut zt)
  -- if nt = $nunpack(zt)
  -- if $nbytes(nt, c) = $data(z, y).DATA[j : $zsize(zt)/8]

rule Step_read/array.init_data-vec:
  z; (REF.ARRAY_ADDR a) (CONST I32 i) (CONST I32 j) (CONST I32 n) (ARRAY.INIT_DATA x y)  ~> ...
  -- otherwise
  -- Expand: $type(z, x) ~~ ARRAY (mut zt)
  -- if vt = $vunpack(vt)
  -- if $vbytes(vt, c) = $data(z, y).DATA[j : $zsize(zt)/8]

The otherwise premise in the vec case negates all the premises in the num case, which also negates Expand: $type(z, x) ~~ ARRAY (mut zt). Therefore, the vec case is unreachable resulting in it not being generated.

To address this issue, I introduced 'consttype.' Does that make sense? (Additionally, I think ot is not a suitable name for consttype. Do you have any alternatives?)