Crash on cyclic bindings

[rossberg]

When variable dependencies in side conditions are cyclic, the interpreter just "crashes" with a Not_found exception instead of producing a useful error message. See #113 for some context.

[f52985]

Resolved by b610769.

FYI: It can kinda pinpoint the exact part where cyclic binding may occur. For example, dropping the forward guess for ma* and making the cyclic binding as in

def $allocmodule(store, module, externval*, val*, ref*, (ref*)*) : (store, moduleinst)
def $allocmodule(s, module, externval*, val_G*, ref_T*, (ref_E*)*) = (s_6, moduleinst)
  -- if module = MODULE type* import* func* global* table* mem* elem* data* start? export*
  -- if func* = (FUNC x local* expr_F)*
  -- if global* = (GLOBAL globaltype expr_G)*
  -- if table* = (TABLE tabletype expr_T)*
  -- if mem* = (MEMORY memtype)*
  -- if elem* = (ELEM elemtype expr_E* elemmode)*
  -- if data* = (DATA byte* datamode)*
  -- if fa_I* = $funcsxv(externval*)
  -- if ga_I* = $globalsxv(externval*)
  -- if ta_I* = $tablesxv(externval*)
  -- if ma_I* = $memsxv(externval*)
  -- if fa* = ($(|s.FUNCS|+i_F))^(i_F<|func*|)
  -- if ga* = ($(|s.GLOBALS|+i_G))^(i_G<|global*|)
  -- if ta* = ($(|s.TABLES|+i_T))^(i_T<|table*|)
;;-- if ma* = ($(|s.MEMS|+i_M))^(i_M<|mem*|)           ;;Making cyclic binding for ma* and modueinst
  -- if ea* = ($(|s.ELEMS|+i_E))^(i_E<|elem*|)
  -- if da* = ($(|s.DATAS|+i_D))^(i_D<|data*|)
  -- if dt* = $alloctypes(type*)
  -- if (s_1, fa*) = $allocfuncs(s, dt*[x]*, (FUNC x local* expr_F)*, moduleinst^(|func*|))     ;; Here
  -- if (s_2, ga*) = $allocglobals(s_1, globaltype*, val_G*)
  -- if (s_3, ta*) = $alloctables(s_2, tabletype*, ref_T*)
  -- if (s_4, ma*) = $allocmems(s_3, memtype*)                                                  ;; Here
  -- if (s_5, ea*) = $allocelems(s_4, elemtype*, (ref_E*)*)
  -- if (s_6, da*) = $allocdatas(s_5, OK^(|data*|), (byte*)*)
  -- if xi* = $allocexports({FUNCS fa_I* fa*, GLOBALS ga_I* ga*, TABLES ta_I* ta*, MEMS ma_I* ma*}, export*)
  -- if moduleinst = {                                                                          ;; And here
      TYPES dt*,
      FUNCS fa_I* fa*, \
      GLOBALS ga_I* ga*,
      TABLES ta_I* ta*, \
      MEMS ma_I* ma*,
      ELEMS ea*, \
      DATAS da*,
      EXPORTS xi*
    }

gives the error message: spec/wasm-3.0/9-module.watsup:116.6-133.6: prose translation error: There might be a cyclic binding,

where the line 116~133 only refers to the last 8 premises, instead of the entire premises.

[rossberg]

Excellent, thanks!