search

alegnani / pancake-verifier

2 stars 0 forks source link

Shared memory modeling #8

Open alegnani opened 1 month ago

JunmingZhao42 commented 1 month ago

Currently in Pancake there're 8-bit, 32-bit and word size shared memory load and store operations (!ld8, !st8, !ld32, !st32, !ldw, !stw). It'd be nice to have some range spec for the shared memory operations correspondingly, for example something like:

method shared_load8(address: Int) returns (value: Int)
  ensures value >= 0 && value < 255
alegnani commented 1 month ago

Do we want something similar for stores e.g. precondition that requires value to be in certain range? Or do we just take the lower 8, 32 or 64 bits?

JunmingZhao42 commented 1 month ago

Do we want something similar for stores e.g. precondition that requires value to be in certain range? Or do we just take the lower 8, 32 or 64 bits?

I think Pancake itself is the latter one (i.e. Pancake doesn't stop user storing a larger range when using !st8 !st32). For the current ethernet driver I think we can check the range of variables using assertions in other places.

(Although for word size load/store that's probably more related to issue #34...)