runtimeverification / iele-semantics

Semantics of Virtual Machine for IELE prototype blockchain
Other
131 stars 33 forks source link

Weirdness in processing numbered registers #149

Open vsubhuman opened 6 years ago

vsubhuman commented 6 years ago

Hello! Am I fundamentally misunderstanding something about registers named by integers ("numbered" registers), or is there something wrong?


I am deploying this contract:

contract Test {
    define @init() {}
    define public @foo(%10) {
        ret %10, %"10"
    }
}

What is the expected result of the @foo(5) call? In reality I get the result: [0, 5] (https://i.imgur.com/RWHBYOk.png) (With named registers: https://i.imgur.com/44BWC7B.png)


Then I deploy this contract:

contract Test {
    define @init() {}
    define public @foo(%10) {
        %20 = %10
        ret %20, %"20"
    }
}

What is the expected result of calling @foo(5)? After the previous example I would expect maybe: [0,0] Actual result: [0,5] (https://i.imgur.com/qUrqg80.png) (With named registers: https://i.imgur.com/Rpk1TSf.png)


So it seems that in return statements numbered registers only work when they are in quotes, hmmmm. Then I deploy this contract:

contract Test {
    define @init() {}
    define public @foo(%10) {
        %20 = %"10"
        ret %20, %"20"
    }
}

It's the same as previous one, but reference to register %10 is not quoted. What is the expected result of calling @foo(5)? After two previous results I would expect: [0, 5] Actual result: [5, 0] (https://i.imgur.com/ZjC0RCQ.png) (With named registers: https://i.imgur.com/WcSPgQl.png)


So it seems that a numbered argument may be referenced in return by being quoted. And if it reassigned to other register without quotes - then this new register also can be referenced in return only with quotes. But if it was reassigned with quotes - then new register can be used in return without quotes. Well, it's weird, but at least we can see the pattern, and now we can verify it. So I deploy this contract:

contract Test {
    define @init() {}
    define public @foo(%10) {
        %20 = %10
        %30 = %"10"
        ret %10, %"10", %20, %"20", %30, %"30"
    }
}

What is the expected result of calling @foo(5)? According to out pattern it should be: [0, 5, 0, 5, 5, 0] Actual result: [0, 5, 0, 0, 5, 0] (https://i.imgur.com/gjCTQHq.png) Wait, what happened to the %20 register? (With named registers: https://i.imgur.com/8Glohmo.png)


Other notable examples:

  1. Trying to mix numbered and named registers: https://i.imgur.com/t5F7viL.png
  2. Mixing them other way around: https://i.imgur.com/bZRPwrm.png (all valid)
  3. Chain-reassignment: https://i.imgur.com/VtB8wPO.png

And idk what this one even is!!!

https://i.imgur.com/IExLm28.png

The same example with named registers:

https://i.imgur.com/6j5aooM.png

image