lmntal / slim

slim LMNtal implementation
Other
18 stars 5 forks source link

Set module が M1 Mac で Segmentation fault する. #294

Open sano-jin opened 1 year ago

sano-jin commented 1 year ago

Set module が M1 Mac で Segmentation fault します.

Problem

以下のプログラムを set2.lmn とする.

ret = set.to_list(set.copy(set.insert(set.insert(set.init, 1), 2), X)).
ret = X

このとき,M1 Mac 上で, slim --use-builtin-rule set2.lmn を実行すると,

[1]    39254 segmentation fault  /.../slim/bin/slim --use-builtin-rule set2.lmn

となる.

-t option をつけて実行すると,以下のようになる.

slim --use-builtin-rule -t set2.lmn
1: ret(set.to_list(set.copy(set.insert(set.insert(set.init,1),2),ret))). @41.
---->_Rets
2: ret(set.to_list(set.copy(set.insert(set.insert(set_empty,1),2),ret))). @41.
---->_Rets
3: ret(set.to_list(set.copy(set.insert(<set>,2),ret))). @41.
---->_Rets
4: ret(set.to_list(set.copy(<set>,ret))). @41.
---->_Rets
5: ret(set.to_list(<set>)). ret(<set>). @41.
[1]    39246 segmentation fault  /.../slim/bin/slim --use-builtin-rule -t set2.lmn

正常に動作するパターン

M1 Mac 以外では,上記のプログラムは正常動作する様子である. 例えば,parmigiano では,以下のような正しい結果を得る.

ret([1,2]). ret(<set>). @41.

また,M1 Mac でも,以下のプログラムは正常動作する.

ret = set.to_list(set.copy(set.insert(set.init, 2), X)).
ret = X

この結果は

ret([105553131559328]). ret(<set>). @41.

となる(正常).

sano-jin commented 1 year ago

このために,M1 Mac 上では, ( slim_finalize をコメントアウトしても) make check に失敗します.