diff --git a/evm-testcases/cfs/while/report.json b/evm-testcases/cfs/while/report.json index 68da929f8..510c9c890 100644 --- a/evm-testcases/cfs/while/report.json +++ b/evm-testcases/cfs/while/report.json @@ -3,14 +3,14 @@ "files" : [ "report.json", "untyped_program.evm-testcases_cfs_while_while_eth.sol().json" ], "info" : { "cfgs" : "1", - "duration" : "23ms", - "end" : "2025-02-26T11:44:06.360+01:00", + "duration" : "281ms", + "end" : "2025-03-17T15:38:36.216+01:00", "expressions" : "6", "files" : "1", "globals" : "0", "members" : "1", "programs" : "1", - "start" : "2025-02-26T11:44:06.337+01:00", + "start" : "2025-03-17T15:38:35.935+01:00", "statements" : "16", "units" : "0", "version" : "0.1", diff --git a/evm-testcases/cfs/while/untyped_program.evm-testcases_cfs_while_while_eth.sol().json b/evm-testcases/cfs/while/untyped_program.evm-testcases_cfs_while_while_eth.sol().json index 619f5aa3f..285e7d7a0 100644 --- a/evm-testcases/cfs/while/untyped_program.evm-testcases_cfs_while_while_eth.sol().json +++ b/evm-testcases/cfs/while/untyped_program.evm-testcases_cfs_while_while_eth.sol().json @@ -1 +1 @@ -{"name":"untyped program::evm-testcases/cfs/while/while_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x00"},{"id":1,"text":"0x00"},{"id":2,"text":"JUMPDEST"},{"id":3,"subNodes":[4],"text":"PUSH1 0x03"},{"id":4,"text":"0x03"},{"id":5,"text":"DUP2"},{"id":6,"text":"LT"},{"id":7,"subNodes":[8],"text":"PUSH1 0x0D"},{"id":8,"text":"0x0D"},{"id":9,"text":"JUMPI"},{"id":10,"subNodes":[11],"text":"PUSH1 0x14"},{"id":11,"text":"0x14"},{"id":12,"text":"JUMP"},{"id":13,"text":"JUMPDEST"},{"id":14,"subNodes":[15],"text":"PUSH1 0x01"},{"id":15,"text":"0x01"},{"id":16,"text":"ADD"},{"id":17,"subNodes":[18],"text":"PUSH1 0x02"},{"id":18,"text":"0x02"},{"id":19,"text":"JUMP"},{"id":20,"text":"JUMPDEST"},{"id":21,"text":"STOP"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":10,"kind":"FalseEdge"},{"sourceId":9,"destId":13,"kind":"TrueEdge"},{"sourceId":10,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":20,"kind":"SequentialEdge"},{"sourceId":13,"destId":14,"kind":"SequentialEdge"},{"sourceId":14,"destId":16,"kind":"SequentialEdge"},{"sourceId":16,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":19,"kind":"SequentialEdge"},{"sourceId":19,"destId":2,"kind":"SequentialEdge"},{"sourceId":20,"destId":21,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":1,"description":{"expressions":["\"0x00\""],"state":"#TOP#"}},{"nodeId":2,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":3,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":4,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":5,"description":{"expressions":["dup2 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":6,"description":{"expressions":["lt 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":7,"description":{"expressions":["push \"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 13]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":8,"description":{"expressions":["\"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":9,"description":{"expressions":["jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]],[[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":10,"description":{"expressions":["push \"0x14\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 20]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":11,"description":{"expressions":["\"0x14\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":12,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":13,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":14,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":15,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":16,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":17,"description":{"expressions":["push \"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":18,"description":{"expressions":["\"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":19,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":20,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":21,"description":"#TOP#"}]} \ No newline at end of file +{"name":"untyped program::evm-testcases/cfs/while/while_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x00"},{"id":1,"text":"0x00"},{"id":2,"text":"JUMPDEST"},{"id":3,"subNodes":[4],"text":"PUSH1 0x03"},{"id":4,"text":"0x03"},{"id":5,"text":"DUP2"},{"id":6,"text":"LT"},{"id":7,"subNodes":[8],"text":"PUSH1 0x0D"},{"id":8,"text":"0x0D"},{"id":9,"text":"JUMPI"},{"id":10,"subNodes":[11],"text":"PUSH1 0x14"},{"id":11,"text":"0x14"},{"id":12,"text":"JUMP"},{"id":13,"text":"JUMPDEST"},{"id":14,"subNodes":[15],"text":"PUSH1 0x01"},{"id":15,"text":"0x01"},{"id":16,"text":"ADD"},{"id":17,"subNodes":[18],"text":"PUSH1 0x02"},{"id":18,"text":"0x02"},{"id":19,"text":"JUMP"},{"id":20,"text":"JUMPDEST"},{"id":21,"text":"STOP"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":10,"kind":"FalseEdge"},{"sourceId":9,"destId":13,"kind":"TrueEdge"},{"sourceId":10,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":20,"kind":"SequentialEdge"},{"sourceId":13,"destId":14,"kind":"SequentialEdge"},{"sourceId":14,"destId":16,"kind":"SequentialEdge"},{"sourceId":16,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":19,"kind":"SequentialEdge"},{"sourceId":19,"destId":2,"kind":"SequentialEdge"},{"sourceId":20,"destId":21,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":1,"description":{"expressions":["\"0x00\""],"state":"#TOP#"}},{"nodeId":2,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":3,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":4,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":5,"description":{"expressions":["dup2 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":6,"description":{"expressions":["lt 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":7,"description":{"expressions":["push \"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 13], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 13]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":8,"description":{"expressions":["\"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":9,"description":{"expressions":["jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":10,"description":{"expressions":["push \"0x14\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 20]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":11,"description":{"expressions":["\"0x14\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":12,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":13,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":14,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":15,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":16,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":17,"description":{"expressions":["push \"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":18,"description":{"expressions":["\"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":19,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":20,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":21,"description":"#TOP#"}]} \ No newline at end of file diff --git a/evm-testcases/cfs/while_npbj/report.json b/evm-testcases/cfs/while_npbj/report.json index 5c4d391d7..314a4d072 100644 --- a/evm-testcases/cfs/while_npbj/report.json +++ b/evm-testcases/cfs/while_npbj/report.json @@ -3,14 +3,14 @@ "files" : [ "report.json", "untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json" ], "info" : { "cfgs" : "1", - "duration" : "116ms", - "end" : "2025-02-26T11:44:06.312+01:00", + "duration" : "416ms", + "end" : "2025-03-17T15:37:51.705+01:00", "expressions" : "9", "files" : "1", "globals" : "0", "members" : "1", "programs" : "1", - "start" : "2025-02-26T11:44:06.196+01:00", + "start" : "2025-03-17T15:37:51.289+01:00", "statements" : "22", "units" : "0", "version" : "0.1", diff --git a/evm-testcases/cfs/while_npbj/untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json b/evm-testcases/cfs/while_npbj/untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json index 8ebbaca20..d18444cf1 100644 --- a/evm-testcases/cfs/while_npbj/untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json +++ b/evm-testcases/cfs/while_npbj/untyped_program.evm-testcases_cfs_while_npbj_while_npbj_eth.sol().json @@ -1 +1 @@ -{"name":"untyped program::evm-testcases/cfs/while_npbj/while_npbj_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x00"},{"id":1,"text":"0x00"},{"id":2,"text":"JUMPDEST"},{"id":3,"subNodes":[4],"text":"PUSH1 0x03"},{"id":4,"text":"0x03"},{"id":5,"text":"DUP2"},{"id":6,"text":"LT"},{"id":7,"subNodes":[8],"text":"PUSH1 0x10"},{"id":8,"text":"0x10"},{"id":9,"subNodes":[10],"text":"PUSH1 0x03"},{"id":10,"text":"0x03"},{"id":11,"text":"ADD"},{"id":12,"text":"JUMPI"},{"id":13,"subNodes":[14],"text":"PUSH1 0x10"},{"id":14,"text":"0x10"},{"id":15,"subNodes":[16],"text":"PUSH1 0x0D"},{"id":16,"text":"0x0D"},{"id":17,"text":"ADD"},{"id":18,"text":"JUMP"},{"id":19,"text":"JUMPDEST"},{"id":20,"subNodes":[21],"text":"PUSH1 0x01"},{"id":21,"text":"0x01"},{"id":22,"text":"ADD"},{"id":23,"subNodes":[24],"text":"PUSH1 0x00"},{"id":24,"text":"0x00"},{"id":25,"subNodes":[26],"text":"PUSH1 0x02"},{"id":26,"text":"0x02"},{"id":27,"text":"ADD"},{"id":28,"text":"JUMP"},{"id":29,"text":"JUMPDEST"},{"id":30,"text":"STOP"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":11,"kind":"SequentialEdge"},{"sourceId":11,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":13,"kind":"FalseEdge"},{"sourceId":12,"destId":19,"kind":"TrueEdge"},{"sourceId":13,"destId":15,"kind":"SequentialEdge"},{"sourceId":15,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":18,"kind":"SequentialEdge"},{"sourceId":18,"destId":29,"kind":"SequentialEdge"},{"sourceId":19,"destId":20,"kind":"SequentialEdge"},{"sourceId":20,"destId":22,"kind":"SequentialEdge"},{"sourceId":22,"destId":23,"kind":"SequentialEdge"},{"sourceId":23,"destId":25,"kind":"SequentialEdge"},{"sourceId":25,"destId":27,"kind":"SequentialEdge"},{"sourceId":27,"destId":28,"kind":"SequentialEdge"},{"sourceId":28,"destId":2,"kind":"SequentialEdge"},{"sourceId":29,"destId":30,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":1,"description":{"expressions":["\"0x00\""],"state":"#TOP#"}},{"nodeId":2,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":3,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":4,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":5,"description":{"expressions":["dup2 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":6,"description":{"expressions":["lt 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":7,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":8,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":9,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":10,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":11,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 19]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":12,"description":{"expressions":["jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]],[[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":13,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":14,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":15,"description":{"expressions":["push \"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16, 13]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":16,"description":{"expressions":["\"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":17,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 29]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":18,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":19,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":20,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":21,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":22,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":23,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":24,"description":{"expressions":["\"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":25,"description":{"expressions":["push \"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":26,"description":{"expressions":["\"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":27,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":28,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":29,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":30,"description":"#TOP#"}]} \ No newline at end of file +{"name":"untyped program::evm-testcases/cfs/while_npbj/while_npbj_eth.sol()","description":null,"nodes":[{"id":0,"subNodes":[1],"text":"PUSH1 0x00"},{"id":1,"text":"0x00"},{"id":2,"text":"JUMPDEST"},{"id":3,"subNodes":[4],"text":"PUSH1 0x03"},{"id":4,"text":"0x03"},{"id":5,"text":"DUP2"},{"id":6,"text":"LT"},{"id":7,"subNodes":[8],"text":"PUSH1 0x10"},{"id":8,"text":"0x10"},{"id":9,"subNodes":[10],"text":"PUSH1 0x03"},{"id":10,"text":"0x03"},{"id":11,"text":"ADD"},{"id":12,"text":"JUMPI"},{"id":13,"subNodes":[14],"text":"PUSH1 0x10"},{"id":14,"text":"0x10"},{"id":15,"subNodes":[16],"text":"PUSH1 0x0D"},{"id":16,"text":"0x0D"},{"id":17,"text":"ADD"},{"id":18,"text":"JUMP"},{"id":19,"text":"JUMPDEST"},{"id":20,"subNodes":[21],"text":"PUSH1 0x01"},{"id":21,"text":"0x01"},{"id":22,"text":"ADD"},{"id":23,"subNodes":[24],"text":"PUSH1 0x00"},{"id":24,"text":"0x00"},{"id":25,"subNodes":[26],"text":"PUSH1 0x02"},{"id":26,"text":"0x02"},{"id":27,"text":"ADD"},{"id":28,"text":"JUMP"},{"id":29,"text":"JUMPDEST"},{"id":30,"text":"STOP"}],"edges":[{"sourceId":0,"destId":2,"kind":"SequentialEdge"},{"sourceId":2,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":7,"kind":"SequentialEdge"},{"sourceId":7,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":11,"kind":"SequentialEdge"},{"sourceId":11,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":13,"kind":"FalseEdge"},{"sourceId":12,"destId":19,"kind":"TrueEdge"},{"sourceId":13,"destId":15,"kind":"SequentialEdge"},{"sourceId":15,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":18,"kind":"SequentialEdge"},{"sourceId":18,"destId":29,"kind":"SequentialEdge"},{"sourceId":19,"destId":20,"kind":"SequentialEdge"},{"sourceId":20,"destId":22,"kind":"SequentialEdge"},{"sourceId":22,"destId":23,"kind":"SequentialEdge"},{"sourceId":23,"destId":25,"kind":"SequentialEdge"},{"sourceId":25,"destId":27,"kind":"SequentialEdge"},{"sourceId":27,"destId":28,"kind":"SequentialEdge"},{"sourceId":28,"destId":2,"kind":"SequentialEdge"},{"sourceId":29,"destId":30,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":1,"description":{"expressions":["\"0x00\""],"state":"#TOP#"}},{"nodeId":2,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":3,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":4,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":5,"description":{"expressions":["dup2 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 3, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 3, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 3, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":6,"description":{"expressions":["lt 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":7,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":8,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":9,"description":{"expressions":["push \"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":10,"description":{"expressions":["\"0x03\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 16], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":11,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1, 19], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1, 19]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":12,"description":{"expressions":["jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]])","jumpi ([[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]],[])"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":13,"description":{"expressions":["push \"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":14,"description":{"expressions":["\"0x10\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":15,"description":{"expressions":["push \"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16, 13]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":16,"description":{"expressions":["\"0x0D\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 16]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":17,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 29]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":18,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":19,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":20,"description":{"expressions":["push \"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 1]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":21,"description":{"expressions":["\"0x01\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":22,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":23,"description":{"expressions":["push \"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":24,"description":{"expressions":["\"0x00\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":25,"description":{"expressions":["push \"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":26,"description":{"expressions":["\"0x02\""],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 0], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 0]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":27,"description":{"expressions":["add 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3, 2]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":28,"description":{"expressions":["jump 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 1], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 2], [_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":29,"description":{"expressions":["jumpdest 1"],"state":{"heap":"monolith","type":"#TOP#","value":"{ stacks: [[_|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, _|_, 3]], memory: EMPTY, storage: #TOP# }"}}},{"nodeId":30,"description":"#TOP#"}]} \ No newline at end of file diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index ee66ec3e3..5b30b0261 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -13,7 +13,6 @@ import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; import java.util.Arrays; -import java.util.Objects; import java.util.function.Predicate; public class AbstractStack implements ValueDomain, BaseLattice { @@ -26,18 +25,35 @@ public class AbstractStack implements ValueDomain, BaseLattice + * This pointer indicates the position in the array that corresponds to the + * bottom of the stack. Tracks the index of the oldest element in the + * circular array. + */ + private int head; + + /** + * The index representing the next insertion point in the circular array. + *

+ * This pointer is used to identify the top of the stack, where the next + * element will be pushed. + */ + private int tail; /** * Helper method to create and fill an array with a specific element. @@ -53,6 +69,8 @@ private static StackElement[] createFilledArray(int size, StackElement element) */ public AbstractStack() { this(createFilledArray(STACK_LIMIT, StackElement.BOTTOM)); + this.head = 0; + this.tail = 0; } /** @@ -61,7 +79,9 @@ public AbstractStack() { * @param stack the stack of values */ public AbstractStack(StackElement[] stack) { - this.stack = stack; + this.circularArray = stack; + this.head = 0; + this.tail = 0; } @Override @@ -125,7 +145,16 @@ public String toString() { return "BOTTOM"; if (isTop()) return "TOP"; - return Arrays.toString(this.stack); + + StringBuilder sb = new StringBuilder("["); + for (int i = 0; i < STACK_LIMIT; i++) { + int pos = (head + i) % STACK_LIMIT; + sb.append(circularArray[pos]); + if (i < STACK_LIMIT - 1) + sb.append(", "); + } + sb.append("]"); + return sb.toString(); } @Override @@ -142,7 +171,7 @@ public AbstractStack bottom() { public boolean isTop() { if (isBottom()) return false; - for (StackElement element : this.stack) + for (StackElement element : this.circularArray) if (!element.isTop()) return false; return true; @@ -150,12 +179,12 @@ public boolean isTop() { @Override public boolean isBottom() { - return stack == null; + return circularArray == null; } @Override public int hashCode() { - return Objects.hash(Arrays.hashCode(stack)); + return Arrays.hashCode(circularArray); } @Override @@ -166,8 +195,22 @@ public boolean equals(Object obj) { return false; if (getClass() != obj.getClass()) return false; + AbstractStack other = (AbstractStack) obj; - return Arrays.equals(stack, other.stack); + return Arrays.equals(this.circularArray, other.circularArray); + } + + /** + * Get a specific element of the stack. + * + * @param index the index of the element + * + * @return the StackElement at the given index, or BOTTOM if out of bounds + */ + public StackElement get(int index) { + if (index < 0 || index >= STACK_LIMIT) // not valid index + return StackElement.BOTTOM; + return circularArray[(head + index) % STACK_LIMIT]; } @Override @@ -182,53 +225,75 @@ public AbstractStack assume(ValueExpression expression, ProgramPoint src, Progra * @return the StackElement at the top of the stack. */ public StackElement getTop() { - return this.stack[STACK_LIMIT - 1]; // Get the last element + return circularArray[(tail - 1 + STACK_LIMIT) % STACK_LIMIT]; } @Override public AbstractStack clone() { if (isBottom() || isTop()) return this; - return new AbstractStack(stack.clone()); + AbstractStack clone = new AbstractStack(circularArray.clone()); + clone.head = this.head; + clone.tail = this.tail; + return clone; } /** * Pushes the specified element onto the stack. + *

+ * This method inserts the given {@link StackElement} at the tail of the + * circular array, effectively updating the top of the stack. The head of + * the stack is also updated to maintain the circular nature of the + * structure. * - * @param target the element to be pushed onto the stack. + * @param element the element to be pushed onto the stack */ - public void push(StackElement target) { - // Shift all elements one position to the left - System.arraycopy(stack, 1, stack, 0, STACK_LIMIT - 1); - stack[STACK_LIMIT - 1] = target; + public void push(StackElement element) { + circularArray[tail] = element; + tail = (tail + 1) % STACK_LIMIT; + head = (head + 1) % STACK_LIMIT; } /** * Pops the element from the stack. + *

+ * This method removes and returns the topmost element of the stack. After + * popping, the stack structure is adjusted by shifting the head, and the + * previous bottommost element is updated based on the next element. If the + * next element is {@link StackElement#TOP}, the bottom is set to TOP, + * otherwise, it is set to {@link StackElement#BOTTOM}. * - * @return the element at the top of the stack. + * @return the element at the top of the stack before popping */ public StackElement pop() { - StackElement result = stack[STACK_LIMIT - 1]; - // Shift all elements one position to the right - System.arraycopy(stack, 0, stack, 1, STACK_LIMIT - 1); - if (!stack[1].isTop()) - stack[0] = StackElement.BOTTOM; + + int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; + StackElement popped = circularArray[topIndex]; + + // Shift + head = (head - 1 + STACK_LIMIT) % STACK_LIMIT; + int bottomIndex = head; + int secondLogicalIndex = (head + 1) % STACK_LIMIT; + + if (circularArray[secondLogicalIndex].isTop()) + circularArray[bottomIndex] = StackElement.TOP; else - stack[0] = StackElement.TOP; + circularArray[bottomIndex] = StackElement.BOTTOM; - return result; + tail = (head + STACK_LIMIT) % STACK_LIMIT; + circularArray[topIndex] = StackElement.BOTTOM; + + return popped; } + /** + * Performs {@code pos} consecutive {@code pop()} operations on the stack. + * + * @param pos the number of elements to pop from the stack + */ public void popX(int pos) { - // Shift all elements pos position to the right - System.arraycopy(stack, 0, stack, pos, STACK_LIMIT - pos); - - for (int i = 1; i < pos; i++) - if (!stack[i].isTop()) - stack[i - 1] = StackElement.BOTTOM; - else - stack[i - 1] = StackElement.TOP; + for (int i = 0; i < pos; i++) + pop(); } @Override @@ -248,13 +313,12 @@ public AbstractStack glbAux(AbstractStack other) throws SemanticException { @Override public boolean lessOrEqualAux(AbstractStack other) throws SemanticException { - // Starting from the top of the stack and moving downward - for (int i = STACK_LIMIT - 1; i >= 0; i--) { - if (!this.stack[i].lessOrEqual(other.stack[i])) { + for (int i = 0; i < STACK_LIMIT; i++) { + int thisIndex = (tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; + int otherIndex = (other.tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; + if (!this.circularArray[thisIndex].lessOrEqual(other.circularArray[otherIndex])) return false; - } } - return true; } @@ -266,9 +330,11 @@ public boolean lessOrEqualAux(AbstractStack other) throws SemanticException { public StackElement getSecondElement() { if (isBottom()) return StackElement.BOTTOM; - else if (isTop()) + if (isTop()) return StackElement.TOP; - return this.stack[STACK_LIMIT - 2]; + + int secondElementPos = (tail - 2 + STACK_LIMIT) % STACK_LIMIT; + return circularArray[secondElementPos]; } /** @@ -301,10 +367,13 @@ public static int getStackLimit() { * @return {@code true} if between 0 and x-positions of the stack an element * is bottom, {@code false} otherwise. */ + public boolean hasBottomUntil(int x) { - for (int i = 0; i < x; i++) - if (this.stack[(STACK_LIMIT - 1) - i].isBottom()) + for (int i = 0; i < x; i++) { + int pos = (tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; + if (circularArray[pos].isBottom()) return true; + } return false; } @@ -325,20 +394,10 @@ public boolean knowsIdentifier(Identifier id) { public AbstractStack dupX(int x) { if (hasBottomUntil(x)) return bottom(); - - StackElement[] stackArray = this.stack.clone(); - - int topIndex = STACK_LIMIT - 1; - int targetIndex = topIndex - x + 1; - StackElement elementToDuplicate = stackArray[targetIndex]; - - StackElement[] resultArray = new StackElement[STACK_LIMIT]; - - System.arraycopy(stackArray, 1, resultArray, 0, STACK_LIMIT - 1); - - resultArray[topIndex] = elementToDuplicate; - - return new AbstractStack(resultArray); + int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; + AbstractStack clone = clone(); + clone.push(circularArray[posX]); + return clone; } /** @@ -346,22 +405,23 @@ public AbstractStack dupX(int x) { * returns the modified stack. * * @param x The position of the element to swap with the top of the stack. - * + * * @return A new stack with the specified elements swapped. */ public AbstractStack swapX(int x) { if (hasBottomUntil(x + 1)) return bottom(); + x++; + int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; // Index of the + // element to swap + // with + int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; - int topIndex = STACK_LIMIT - 1; - int swapIndex = topIndex - x; - - StackElement[] newStack = this.stack.clone(); - - StackElement temp = newStack[topIndex]; - newStack[topIndex] = newStack[swapIndex]; - newStack[swapIndex] = temp; - - return new AbstractStack(newStack); + AbstractStack clone = clone(); + StackElement temp = clone.circularArray[posX]; + clone.circularArray[posX] = clone.circularArray[topIndex]; + clone.circularArray[topIndex] = temp; + return clone; } + } \ No newline at end of file diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index 7ad3daaab..f8b9b144e 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -11,15 +11,12 @@ import it.unive.lisa.symbolic.value.Constant; import it.unive.lisa.symbolic.value.Identifier; import it.unive.lisa.symbolic.value.Operator; -import it.unive.lisa.symbolic.value.Skip; import it.unive.lisa.symbolic.value.UnaryExpression; import it.unive.lisa.symbolic.value.ValueExpression; import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator; import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredRepresentation; -import java.util.ArrayList; -import java.util.Iterator; -import java.util.List; +import java.util.Arrays; import java.util.Objects; import java.util.Set; import java.util.function.Predicate; @@ -33,9 +30,27 @@ public abstract class TaintAbstractDomain protected static int STACK_LIMIT = 32; /** - * The abstract stack domain. + * The abstract stack as a circular array. */ - private final ArrayList stack; + private final TaintElement[] circularArray; + + /** + * The index representing the beginning of the logical stack in the circular + * array. + *

+ * This pointer indicates the position in the array that corresponds to the + * bottom of the stack. Tracks the index of the oldest element in the + * circular array. + */ + private int head; + + /** + * The index representing the next insertion point in the circular array. + *

+ * This pointer is used to identify the top of the stack, where the next + * element will be pushed. + */ + private int tail; /** * The local memory, tracking if it is clean or tainted. @@ -43,14 +58,17 @@ public abstract class TaintAbstractDomain private final TaintElement memory; /** - * Builds a taint abstract stack starting from a given stack and a list of - * elements that push taint. + * Builds a taint abstract stack starting from a given stack and a memory + * element. * - * @param stack the stack of values + * @param circularArray the stack of values + * @param memory the memory element */ - protected TaintAbstractDomain(ArrayList stack, TaintElement memory) { - this.stack = stack; + protected TaintAbstractDomain(TaintElement[] circularArray, TaintElement memory) { + this.circularArray = circularArray; this.memory = memory; + this.head = 0; + this.tail = 0; } @Override @@ -129,8 +147,7 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement opnd1 = resultStack.pop(); - TaintElement opnd2 = resultStack.pop(); + resultStack.popX(2); return resultStack; } @@ -188,7 +205,8 @@ else if (memory.isClean()) TaintElement value = resultStack.pop(); if (value.isTaint()) - return mk(resultStack.stack, TaintElement.TAINT); + return mk(resultStack.circularArray, TaintElement.TAINT); + else if (value.isClean()) return resultStack; } @@ -197,10 +215,7 @@ else if (value.isClean()) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement destOffset = resultStack.pop(); - TaintElement offset = resultStack.pop(); - TaintElement size = resultStack.pop(); - + resultStack.popX(3); return resultStack; } @@ -256,24 +271,16 @@ else if (value.isClean()) return bottom(); TaintAbstractDomain resultStack = clone(); resultStack.pop(); - - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "SstoreOperator": { // pops 2 if (hasBottomUntil(2)) return bottom(); TaintAbstractDomain resultStack = clone(); - resultStack.pop(); - resultStack.pop(); + resultStack.popX(2); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Dup1Operator": { // DUP1 @@ -376,71 +383,41 @@ else if (value.isClean()) if (hasBottomUntil(2)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(2); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Log1Operator": { // LOG1 if (hasBottomUntil(3)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); - resultStack.pop(); + resultStack.popX(3); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Log2Operator": { // LOG2 if (hasBottomUntil(4)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); - resultStack.pop(); - resultStack.pop(); + resultStack.popX(4); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Log3Operator": { // LOG3 if (hasBottomUntil(5)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); - resultStack.pop(); - resultStack.pop(); - resultStack.pop(); + resultStack.popX(5); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "Log4Operator": { // LOG4 if (hasBottomUntil(6)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); - resultStack.pop(); - resultStack.pop(); - resultStack.pop(); - resultStack.pop(); + resultStack.popX(6); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "CreateOperator": { // CREATE if (hasBottomUntil(3)) @@ -498,10 +475,7 @@ else if (value.isClean()) TaintElement offset = resultStack.pop(); TaintElement length = resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "DelegatecallOperator": case "StaticcallOperator": { // pops 6, push 1 @@ -525,13 +499,9 @@ else if (value.isClean()) if (hasBottomUntil(2)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement offset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(2); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "InvalidOperator": { // INVALID return this; @@ -542,23 +512,15 @@ else if (value.isClean()) TaintAbstractDomain resultStack = clone(); TaintElement recipient = resultStack.pop(); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "CodecopyOperator": { // CODECOPY if (hasBottomUntil(3)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement memOffset = resultStack.pop(); - TaintElement dataOffset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(3); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "ExtcodesizeOperator": { // EXTCODESIZE if (hasBottomUntil(1)) @@ -576,28 +538,17 @@ else if (value.isClean()) if (hasBottomUntil(4)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement address = resultStack.pop(); - TaintElement memOffset = resultStack.pop(); - TaintElement dataOffset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(4); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "ReturndatacopyOperator": { // RETURNDATACOPY if (hasBottomUntil(3)) return bottom(); TaintAbstractDomain resultStack = clone(); - TaintElement memOffset = resultStack.pop(); - TaintElement dataOffset = resultStack.pop(); - TaintElement length = resultStack.pop(); + resultStack.popX(3); - if (resultStack.isEmpty()) - return bottom(); - else - return resultStack; + return resultStack; } case "ExtcodehashOperator": { // EXTCODEHASH if (hasBottomUntil(1)) @@ -615,96 +566,68 @@ else if (value.isClean()) } } - if (!(expression instanceof Skip)) - throw new SemanticException("Reachable just with the skip node"); - - return top(); + throw new SemanticException("Unrecognized opcode: " + pp); } private TaintAbstractDomain dupXoperator(int x, TaintAbstractDomain stack) { if (stack.isEmpty() || stack.hasBottomUntil(x)) return bottom(); - return dupX(x, stack.clone()); + return stack.dupX(x); } private TaintAbstractDomain swapXoperator(int x, TaintAbstractDomain stack) { - if (stack.isEmpty() || stack.hasBottomUntil(x)) + if (stack.isEmpty() || stack.hasBottomUntil(x + 1)) return bottom(); - return swapX(x, stack.clone()); + return stack.swapX(x); } - private TaintAbstractDomain swapX(int x, TaintAbstractDomain stack) { - List clone = stack.clone().getStack(); - - if (stack.size() < x + 1 || x < 1) - return stack.bottom(); - - Object[] obj = clone.toArray(); - int first; - - if (stack.size() < STACK_LIMIT) - first = STACK_LIMIT - 1; - else - first = clone.size() - 1; - - Object tmp = obj[first]; - obj[first] = obj[first - x]; - obj[first - x] = tmp; - - ArrayList result = new ArrayList<>(); - - for (int i = 0; i < clone.size(); i++) - result.add((TaintElement) obj[i]); - - return mk(result, stack.memory); - } - - private TaintAbstractDomain dupX(int x, TaintAbstractDomain stack) { - List clone = stack.clone().getStack(); - - if (stack.size() < x || x < 1) - return stack.bottom(); - - Object[] obj = clone.toArray(); - - int first; - if (stack.size() < STACK_LIMIT) - first = STACK_LIMIT; - else - first = clone.size(); - - TaintElement tmp = (TaintElement) obj[first - x]; - - ArrayList result = new ArrayList<>(); - - for (int i = 0; i < clone.size(); i++) - result.add((TaintElement) obj[i]); - - result.add(tmp); - result.remove(0); - - return mk(result, stack.memory); - } - - private ArrayList getStack() { - return stack; + /** + * Checks whether the stack is empty. + * + * @return {@code true} if the first element is bottom, {@code false} + * otherwise. + */ + public boolean isEmpty() { + return getFirstElement().isBottom(); } - private int size() { - int bottomCounter = 0; - for (TaintElement item : stack) { - if (item.isBottom()) { - bottomCounter++; - } - } - return stack.size() - bottomCounter; + /** + * Swaps the 1st with the (x + 1)-th element from the top of the stack and + * returns the modified stack. + * + * @param x The position of the element to swap with the top of the stack. + * + * @return A new stack with the specified elements swapped. + */ + public TaintAbstractDomain swapX(int x) { + if (hasBottomUntil(x + 1)) + return bottom(); + x++; + int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; + int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; + TaintAbstractDomain copy = this.clone(); + TaintElement tmp = copy.circularArray[posX]; + copy.circularArray[posX] = copy.circularArray[topIndex]; + copy.circularArray[topIndex] = tmp; + return copy; } - private boolean isEmpty() { - if (!stack.isEmpty()) - return false; - else - return true; + /** + * Duplicates the x-th element from the top of the stack and returns the + * modified stack. + * + * @param x The position of the element to duplicate from the top of the + * stack. + * + * @return A new stack with the specified element duplicated at the top. + */ + public TaintAbstractDomain dupX(int x) { + if (hasBottomUntil(x)) + return bottom(); + int posX = (tail - x + STACK_LIMIT) % STACK_LIMIT; + TaintAbstractDomain copy = this.clone(); + copy.push(circularArray[posX]); + return copy; } @Override @@ -746,17 +669,24 @@ public StructuredRepresentation representation() { else if (isTop()) return Lattice.topRepresentation(); - return new StringRepresentation(stack.toString()); + return new StringRepresentation(this.toString()); } @Override public String toString() { if (isBottom()) return Lattice.BOTTOM_STRING; - else if (isTop()) + if (isTop()) return Lattice.TOP_STRING; - - return stack.toString(); + StringBuilder sb = new StringBuilder("["); + for (int i = 0; i < STACK_LIMIT; i++) { + int pos = (head + i) % STACK_LIMIT; + sb.append(circularArray[pos]); + if (i < STACK_LIMIT - 1) + sb.append(", "); + } + sb.append("]"); + return sb.toString(); } @Override @@ -771,75 +701,107 @@ public TaintAbstractDomain popScope(ScopeToken token) throws SemanticException { return this; } + /** + * Computes the greatest lower bound (GLB) between this abstract domain and + * another. + * + * @param other the other domain + * + * @return a new domain representing the greatest lower bound of the two + * domains + */ @Override public TaintAbstractDomain glbAux(TaintAbstractDomain other) throws SemanticException { - ArrayList result = new ArrayList<>(STACK_LIMIT); - - Iterator thisIterator = this.stack.iterator(); - Iterator otherIterator = other.stack.iterator(); - - while (thisIterator.hasNext() && otherIterator.hasNext()) { - TaintElement thisElement = thisIterator.next(); - TaintElement otherElement = otherIterator.next(); - result.add(thisElement.glb(otherElement)); + TaintElement[] result = new TaintElement[STACK_LIMIT]; + for (int i = 0; i < STACK_LIMIT; i++) { + result[i] = this.get(i).glb(other.get(i)); } - return mk(result, this.memory.glb(other.memory)); } + /** + * Computes the least upper bound (LUB) between this abstract domain and + * another. + * + * @param other the other domain + * + * @return a new domain representing the least upper bound of the two + * domains + */ @Override public TaintAbstractDomain lubAux(TaintAbstractDomain other) throws SemanticException { - ArrayList result = new ArrayList<>(STACK_LIMIT); - - Iterator thisIterator = this.stack.iterator(); - Iterator otherIterator = other.stack.iterator(); - - while (thisIterator.hasNext() && otherIterator.hasNext()) { - TaintElement thisElement = thisIterator.next(); - TaintElement otherElement = otherIterator.next(); - result.add(thisElement.lub(otherElement)); + TaintElement[] result = new TaintElement[STACK_LIMIT]; + for (int i = 0; i < STACK_LIMIT; i++) { + result[i] = this.get(i).lub(other.get(i)); } - return mk(result, this.memory.lub(other.memory)); } + /** + * Get a specific element of the stack. + * + * @param index the index of the element + * + * @return the StackElement at the given index, or BOTTOM if out of bounds + */ + public TaintElement get(int index) { + if (index < 0 || index >= STACK_LIMIT) + return TaintElement.BOTTOM; + return circularArray[(head + index) % STACK_LIMIT]; + } + @Override public boolean lessOrEqualAux(TaintAbstractDomain other) throws SemanticException { - Iterator thisIterator = this.stack.iterator(); - Iterator otherIterator = other.stack.iterator(); - - while (thisIterator.hasNext() && otherIterator.hasNext()) { - if (!thisIterator.next().lessOrEqual(otherIterator.next())) { + for (int i = 0; i < STACK_LIMIT; i++) + if (!this.get(i).lessOrEqual(other.get(i))) return false; - } - } return true; } /** * Pushes the specified element onto the stack. + *

+ * This method inserts the given {@link TaintElement} at the tail of the + * circular array, effectively updating the top of the stack. The head of + * the stack is also updated to maintain the circular nature of the + * structure. * - * @param target the element to be pushed onto the stack. + * @param target the element to be pushed onto the stack */ public void push(TaintElement target) { - stack.remove(0); - stack.add(target); + circularArray[tail] = target; + tail = (tail + 1) % STACK_LIMIT; + head = (head + 1) % STACK_LIMIT; } /** * Pops the element from the stack. + *

+ * This method removes and returns the topmost element of the stack. After + * popping, the stack structure is adjusted by shifting the head, and the + * previous bottommost element is updated based on the next element. If the + * next element is {@link TaintElement#TOP}, the bottom is set to TOP, + * otherwise, it is set to {@link TaintElement#BOTTOM}. * - * @return the element at the top of the stack. + * @return the element at the top of the stack before popping */ public TaintElement pop() { - TaintElement result = stack.remove(stack.size() - 1); - if (stack.get(0).isBottom()) - stack.add(0, TaintElement.BOTTOM); + int topIndex = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; + TaintElement popped = circularArray[topIndex]; + + head = (head - 1 + STACK_LIMIT) % STACK_LIMIT; + int bottomIndex = head; + int nextIndex = (head + 1) % STACK_LIMIT; + + if (circularArray[nextIndex].isTop()) + circularArray[bottomIndex] = TaintElement.TOP; else - stack.add(0, TaintElement.TOP); + circularArray[bottomIndex] = TaintElement.BOTTOM; + tail = (tail - 1 + STACK_LIMIT) % STACK_LIMIT; + circularArray[topIndex] = TaintElement.BOTTOM; - return result; + return popped; } /** @@ -853,55 +815,84 @@ public TaintElement pop() { * is bottom, {@code false} otherwise. */ public boolean hasBottomUntil(int x) { - for (int i = 0; i < x; i++) - if (this.stack.get((STACK_LIMIT - 1) - i).isBottom()) + for (int i = 0; i < x; i++) { + int index = (tail - 1 - i + STACK_LIMIT) % STACK_LIMIT; + if (circularArray[index].isBottom()) return true; + } return false; } @Override public TaintAbstractDomain clone() { - if (isBottom()) - return this; - return mk(new ArrayList<>(stack), this.memory); + TaintElement[] newArray = circularArray.clone(); + TaintAbstractDomain copy = mk(newArray, memory); + copy.head = this.head; + copy.tail = this.tail; + return copy; } @Override public boolean equals(Object obj) { if (this == obj) return true; - if (obj == null) - return false; - if (getClass() != obj.getClass()) + if (!(obj instanceof TaintAbstractDomain)) return false; TaintAbstractDomain other = (TaintAbstractDomain) obj; - return Objects.equals(memory, other.memory) && Objects.equals(stack, other.stack); + + if (isBottom() || other.isBottom()) + return isBottom() == other.isBottom(); + + if (!memory.equals(other.memory)) + return false; + + return Arrays.equals(this.circularArray, other.circularArray); } @Override public int hashCode() { - return Objects.hash(memory, stack); + return Objects.hash(circularArray, memory); } + /** + * Yields the second element of this abstract stack. + * + * @return the second element of this abstract stack + */ public TaintElement getSecondElement() { if (isBottom()) return TaintElement.BOTTOM; - else if (isTop()) + if (isTop()) return TaintElement.TOP; - return this.stack.get(STACK_LIMIT - 2); + return circularArray[(tail - 2 + STACK_LIMIT) % STACK_LIMIT]; } + /** + * Yields the first element of this abstract stack. + * + * @return the first element of this abstract stack + */ public TaintElement getFirstElement() { if (isBottom()) return TaintElement.BOTTOM; - else if (isTop()) + if (isTop()) return TaintElement.TOP; - return this.stack.get(STACK_LIMIT - 1); + return circularArray[(tail - 1 + STACK_LIMIT) % STACK_LIMIT]; + } + + /** + * Performs {@code pos} consecutive {@code pop()} operations on the stack. + * + * @param pos the number of elements to pop from the stack + */ + public void popX(int pos) { + for (int i = 0; i < pos; i++) + pop(); } /** * Yields the set of opcodes that push taint elements. - * + * * @return the set of opcodes that push taint elements */ public abstract Set getTaintedOpcode(); @@ -916,12 +907,12 @@ else if (isTop()) /** * Utility for creating a concrete instance of {@link TaintAbstractDomain} * given the stack and the memory. - * - * @param list the stack + * + * @param array the stack * @param memory the memory - * + * * @return a new concrete instance of {@link TaintAbstractDomain} */ - public abstract TaintAbstractDomain mk(ArrayList list, TaintElement memory); + public abstract TaintAbstractDomain mk(TaintElement[] array, TaintElement memory); } \ No newline at end of file diff --git a/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java index 8c0cd8595..3af779d58 100644 --- a/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TimestampDependencyAbstractDomain.java @@ -5,33 +5,35 @@ import it.unipr.analysis.operator.DifficultyOperator; import it.unipr.analysis.operator.TimestampOperator; import it.unive.lisa.symbolic.value.Operator; -import java.util.ArrayList; -import java.util.Collections; -import java.util.HashSet; -import java.util.Set; +import java.util.*; public class TimestampDependencyAbstractDomain extends TaintAbstractDomain { private static final TimestampDependencyAbstractDomain TOP = new TimestampDependencyAbstractDomain( - new ArrayList<>(Collections.nCopies(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM)), - TaintElement.CLEAN); + createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); private static final TimestampDependencyAbstractDomain BOTTOM = new TimestampDependencyAbstractDomain(null, TaintElement.BOTTOM); + private static TaintElement[] createFilledArray(int size, TaintElement element) { + TaintElement[] array = new TaintElement[size]; + Arrays.fill(array, element); + return array; + } + /** * Builds an initial symbolic stack. */ public TimestampDependencyAbstractDomain() { - this(new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM)), TaintElement.CLEAN); + this(createFilledArray(STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); } /** * Builds a taint abstract stack starting from a given stack and a list of * elements that push taint. * - * @param stack the stack of values + * @param circularArray the stack of values */ - protected TimestampDependencyAbstractDomain(ArrayList stack, TaintElement memory) { - super(stack, memory); + protected TimestampDependencyAbstractDomain(TaintElement[] circularArray, TaintElement memory) { + super(circularArray, memory); } @Override @@ -60,8 +62,8 @@ public TimestampDependencyAbstractDomain bottom() { } @Override - public TaintAbstractDomain mk(ArrayList list, TaintElement memory) { - return new TimestampDependencyAbstractDomain(list, memory); + public TaintAbstractDomain mk(TaintElement[] array, TaintElement memory) { + return new TimestampDependencyAbstractDomain(array, memory); } } \ No newline at end of file diff --git a/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java index 7a66d56db..6cf263c60 100644 --- a/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java @@ -2,32 +2,37 @@ import it.unipr.analysis.operator.OriginOperator; import it.unive.lisa.symbolic.value.Operator; -import java.util.ArrayList; +import java.util.Arrays; import java.util.Collections; import java.util.Set; public class TxOriginAbstractDomain extends TaintAbstractDomain { private static final TxOriginAbstractDomain TOP = new TxOriginAbstractDomain( - new ArrayList<>(Collections.nCopies(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM)), - TaintElement.CLEAN); + createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); private static final TxOriginAbstractDomain BOTTOM = new TxOriginAbstractDomain(null, TaintElement.BOTTOM); + private static TaintElement[] createFilledArray(int size, TaintElement element) { + TaintElement[] array = new TaintElement[size]; + Arrays.fill(array, element); + return array; + } + /** * Builds an initial symbolic stack. */ public TxOriginAbstractDomain() { - this(new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM)), TaintElement.CLEAN); + this(createFilledArray(STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); } /** * Builds a taint abstract stack starting from a given stack and a list of * elements that push taint. * - * @param stack the stack of values + * @param circularArray the stack of values */ - protected TxOriginAbstractDomain(ArrayList stack, TaintElement memory) { - super(stack, memory); + protected TxOriginAbstractDomain(TaintElement[] circularArray, TaintElement memory) { + super(circularArray, memory); } @Override @@ -51,7 +56,7 @@ public TxOriginAbstractDomain bottom() { } @Override - public TaintAbstractDomain mk(ArrayList list, TaintElement memory) { - return new TxOriginAbstractDomain(list, memory); + public TaintAbstractDomain mk(TaintElement[] array, TaintElement memory) { + return new TxOriginAbstractDomain(array, memory); } }