search

runtimeverification / polkadot-verification

Verification of Polkadot WASM code
Other
9 stars 6 forks source link

Search script - randomly test Polkadot sources #84

Closed ehildenb closed 4 years ago

ehildenb commented 4 years ago

Blocked on #81

ehildenb commented 4 years ago

Main difficulties were in making sure we didn't hit the Python recursion limit, but seem to have found a way to make sure we don't.

Demi-Marie commented 4 years ago

Can we avoid using recursion at all?

ehildenb commented 4 years ago

Well, the issue is that the pyk library recurses over the term to print it out to the screen (here: https://github.com/kframework/k/blob/master/k-distribution/src/main/scripts/lib/pyk/kast.py#L270). Rewriting this algorithm iteratively would be fairly difficult, unfortunately.

But I've avoided the issue by figuring out the part of the configuration which caused problems (which took quite a bit of trial and error), and just telling it to not print that part of the configuration. That's what the line which sets final_subst['MEMS_CELL'] to an Omitted token does.

ehildenb commented 4 years ago

Also, this is not as useful without #85 merged, which improves the error messages the LLVM backend gives. I found that one out the hard way.

drskalman commented 4 years ago

couldn't test because of interpreter: /home/user/doc/code/polkadot-verification/deps/wasm-semantics/deps/k/llvm-backend/src/main/native/llvm-backend/runtime/collect/collect.cpp:137: void migrate_mpz(mpz_ptr *): Assertionintgr->i->_mp_alloc * sizeof(mp_limb_t) == lenLimbs' failed. `