Skip to content

Commit

Permalink
Fixed SHR semantic's and updated tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@merendamattia
merendamattia committed Feb 23, 2024
1 parent 7ba1fad commit 1034ba8
Show file tree
Hide file tree
Showing 44 changed files with 117 additions and 84 deletions.
6 changes: 3 additions & 3 deletions evm-testcases/cfs/add/report.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,14 +3,14 @@
"files" : [ "report.json", "untyped_program.evm-testcases_cfs_add_add_eth.sol().json" ],
"info" : {
"cfgs" : "1",
"duration" : "135ms",
"end" : "2024-02-08T10:17:06.409+01:00",
"duration" : "121ms",
"end" : "2024-02-23T10:20:48.169+01:00",
"expressions" : "6",
"files" : "1",
"globals" : "0",
"members" : "1",
"programs" : "1",
"start" : "2024-02-08T10:17:06.274+01:00",
"start" : "2024-02-23T10:20:48.048+01:00",
"statements" : "11",
"units" : "0",
"version" : "0.1b8",
Expand Down
2 changes: 1 addition & 1 deletion evm-testcases/cfs/add/untyped_program.evm-testcases_cfs_add_add_eth.sol().json
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"name":"untyped program::evm-testcases/cfs/add/add_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x10"},{"id":1,"text":"0x10"},{"id":2,"subNodes":[3],"text":"PUSH1 0x10"},{"id":3,"text":"0x10"},{"id":4,"text":"ADD"},{"id":5,"subNodes":[6],"text":"PUSH1 0x20"},{"id":6,"text":"0x20"},{"id":7,"text":"EQ"},{"id":8,"subNodes":[9],"text":"PUSH32 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"},{"id":9,"text":"0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"},{"id":10,"subNodes":[11],"text":"PUSH1 0x01"},{"id":11,"text":"0x01"},{"id":12,"text":"ADD"},{"id":13,"subNodes":[14],"text":"PUSH1 0x00"},{"id":14,"text":"0x00"},{"id":15,"text":"EQ"},{"id":16,"text":"ret"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":4,"kind":"SequentialEdge"},{"sourceId":4,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":8,"kind":"SequentialEdge"},{"sourceId":8,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":13,"kind":"SequentialEdge"},{"sourceId":13,"destId":15,"kind":"SequentialEdge"},{"sourceId":15,"destId":16,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [16]], memory: _|_, mu_i: [0] }"}}},{"nodeId":1,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_], memory: _|_, mu_i: [0] }"}}},{"nodeId":2,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [16], [16]], memory: _|_, mu_i: [0] }"}}},{"nodeId":3,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [16]], memory: _|_, mu_i: [0] }"}}},{"nodeId":4,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [32]], memory: _|_, mu_i: [0] }"}}},{"nodeId":5,"description":{"expressions":["push \"0x20\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [32], [32]], memory: _|_, mu_i: [0] }"}}},{"nodeId":6,"description":{"expressions":["\"0x20\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [32]], memory: _|_, mu_i: [0] }"}}},{"nodeId":7,"description":{"expressions":["eq 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [1]], memory: _|_, mu_i: [0] }"}}},{"nodeId":8,"description":{"expressions":["push \"0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [1], [115792089237316195423570985008687907853269984665640564039457584007913129639935]], memory: _|_, mu_i: [0] }"}}},{"nodeId":9,"description":{"expressions":["\"0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [1]], memory: _|_, mu_i: [0] }"}}},{"nodeId":10,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [1], [115792089237316195423570985008687907853269984665640564039457584007913129639935], [1]], memory: _|_, mu_i: [0] }"}}},{"nodeId":11,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [1], [115792089237316195423570985008687907853269984665640564039457584007913129639935]], memory: _|_, mu_i: [0] }"}}},{"nodeId":12,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [1], [0]], memory: _|_, mu_i: [0] }"}}},{"nodeId":13,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [1], [0], [0]], memory: _|_, mu_i: [0] }"}}},{"nodeId":14,"description":{"expressions":["\"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [1], [0]], memory: _|_, mu_i: [0] }"}}},{"nodeId":15,"description":{"expressions":["eq 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, [1], [1]], memory: _|_, mu_i: [0] }"}}},{"nodeId":16,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stack: [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_], memory: _|_, mu_i: [0] }"}}}]}
{"name":"untyped program::evm-testcases/cfs/add/add_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x10"},{"id":1,"text":"0x10"},{"id":2,"subNodes":[3],"text":"PUSH1 0x10"},{"id":3,"text":"0x10"},{"id":4,"text":"ADD"},{"id":5,"subNodes":[6],"text":"PUSH1 0x20"},{"id":6,"text":"0x20"},{"id":7,"text":"EQ"},{"id":8,"subNodes":[9],"text":"PUSH32 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"},{"id":9,"text":"0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"},{"id":10,"subNodes":[11],"text":"PUSH1 0x01"},{"id":11,"text":"0x01"},{"id":12,"text":"ADD"},{"id":13,"subNodes":[14],"text":"PUSH1 0x00"},{"id":14,"text":"0x00"},{"id":15,"text":"EQ"},{"id":16,"text":"ret"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":4,"kind":"SequentialEdge"},{"sourceId":4,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":8,"kind":"SequentialEdge"},{"sourceId":8,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":13,"kind":"SequentialEdge"},{"sourceId":13,"destId":15,"kind":"SequentialEdge"},{"sourceId":15,"destId":16,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[16]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":1,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":2,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[16], [16]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":3,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[16]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":4,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[32]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":5,"description":{"expressions":["push \"0x20\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[32], [32]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":6,"description":{"expressions":["\"0x20\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[32]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":7,"description":{"expressions":["eq 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[1]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":8,"description":{"expressions":["push \"0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[1], [115792089237316195423570985008687907853269984665640564039457584007913129639935]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":9,"description":{"expressions":["\"0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[1]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":10,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[1], [115792089237316195423570985008687907853269984665640564039457584007913129639935], [1]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":11,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[1], [115792089237316195423570985008687907853269984665640564039457584007913129639935]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":12,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[1], [0]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":13,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[1], [0], [0]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":14,"description":{"expressions":["\"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[1], [0]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":15,"description":{"expressions":["eq 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{[1], [1]}}, memory: _|_, mu_i: [0] }"}}},{"nodeId":16,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: {{}}, memory: _|_, mu_i: [0] }"}}}]}
4 changes: 2 additions & 2 deletions evm-testcases/cfs/addmod/report.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,13 @@
"info" : {
"cfgs" : "1",
"duration" : "2ms",
"end" : "2024-02-08T10:17:06.793+01:00",
"end" : "2024-02-23T10:20:51.153+01:00",
"expressions" : "8",
"files" : "1",
"globals" : "0",
"members" : "1",
"programs" : "1",
"start" : "2024-02-08T10:17:06.791+01:00",
"start" : "2024-02-23T10:20:51.151+01:00",
"statements" : "13",
"units" : "0",
"version" : "0.1b8",
Expand Down
Loading

0 comments on commit 1034ba8

Please sign in to comment.