search

runtimeverification / hs-backend-booster

Accelerates K Framework's Haskell backend
BSD 3-Clause "New" or "Revised" License
7 stars 0 forks source link

Fix unification case between inj and function #544

Closed goodlyrottenapple closed 6 months ago

goodlyrottenapple commented 6 months ago

Fix for https://github.com/runtimeverification/kontrol/issues/418

The issue discovered was the failed unification of 

inj{SortInt{}, SortGas{}}("0")

with 

#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort(
  "false",
  inj{SortInt{},SortGas{}}("0"),
  inj{SortInt{},SortGas{}}("0")
)

which should instead be indeterminate, as the ite does in fact evaluate to inj{SortInt{},SortGas{}}("0")

goodlyrottenapple commented 6 months ago

KEVM

Test sam-unifier-inj-fix time master-cd8bac1 time (sam-unifier-inj-fix/master-cd8bac1) time
kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k 53.84 55.79 0.9650474995518911
mcd/vat-move-diff-rough-spec.k 180.83 171.4 1.055017502917153
TOTAL 234.67000000000002 227.19 1.0329239843302964