Open XiangyuG opened 5 years ago
/tmp/superspreader_canonicalized_equivalent_0.sk file content: |StateAndPacket| program (|StateAndPacket| state_and_packet) { state_and_packet.pkt_0=state_and_packet.pkt_0; if (state_and_packet.pkt_1==1) {state_and_packet.state_group_0_state_0=state_and_packet.state_group_0_state_0+1; if (state_and_packet.state_group_0_state_0==1000) {state_and_packet.state_group_1_state_0=1; ;} ;}else {if (state_and_packet.pkt_1==2) {state_and_packet.state_group_0_state_0=state_and_packet.state_group_0_state_0-1; } } return state_and_packet; } cmd line and results xiangyug@cyclops:~/chipmunk_experiments$ time iterative_solver /tmp/superspreader_canonicalized_equivalent_0.sk example_alus/nested_ifs.stateful_alu stateless_alus/stateless_alu.j2 4 5 10 --parallel-sketch Iteration #1 Total number of hole bits is 952 Sketch file is superspreader_canonicalized_equivalent_0_nested_ifs_stateless_alu_4_5_codegen_iteration_1.sk Synthesis succeeded with 2 bits, proceeding to verification. Verification failed, use returned counterexamples {'pkt_1': 1, 'pkt_0': 0} {'state_group_1_state_0': 0, 'state_group_0_state_0': 999} Iteration #2 Total number of hole bits is 952 Sketch file is superspreader_canonicalized_equivalent_0_nested_ifs_stateless_alu_4_5_codegen_iteration_2.sk Synthesis succeeded with 2 bits, proceeding to verification. Verification failed, use returned counterexamples {'pkt_1': 2, 'pkt_0': 0} {'state_group_1_state_0': 2, 'state_group_0_state_0': 4} Iteration #3 Total number of hole bits is 952 Sketch file is superspreader_canonicalized_equivalent_0_nested_ifs_stateless_alu_4_5_codegen_iteration_3.sk Error in `/usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis': free(): invalid next size (fast): 0x000000000104f660 ======= Backtrace: ========= /lib/x86_64-linux-gnu/libc.so.6(+0x777e5)[0x7f7c4f4607e5] /lib/x86_64-linux-gnu/libc.so.6(+0x8037a)[0x7f7c4f46937a] /lib/x86_64-linux-gnu/libc.so.6(cfree+0x4c)[0x7f7c4f46d53c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d54d] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x42bb71] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x42e618] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x42f654] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x412dd1] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40c93b] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x404bac] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf0)[0x7f7c4f409830] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x405f29] ======= Memory map: ======== 00400000-00563000 r-xp 00000000 fd:00 25432926 /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis 00762000-00763000 r--p 00162000 fd:00 25432926 /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis 00763000-00764000 rw-p 00163000 fd:00 25432926 /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis 00764000-00765000 rw-p 00000000 00:00 0 009ee000-04c22000 rw-p 00000000 00:00 0 [heap] 7f7c40000000-7f7c40021000 rw-p 00000000 00:00 0 7f7c40021000-7f7c44000000 ---p 00000000 00:00 0 7f7c48000000-7f7c48021000 rw-p 00000000 00:00 0 7f7c48021000-7f7c4c000000 ---p 00000000 00:00 0 7f7c4ebe8000-7f7c4ebe9000 ---p 00000000 00:00 0 7f7c4ebe9000-7f7c4f3e9000 rw-p 00000000 00:00 0 7f7c4f3e9000-7f7c4f5a9000 r-xp 00000000 fd:00 42729973 /lib/x86_64-linux-gnu/libc-2.23.so 7f7c4f5a9000-7f7c4f7a9000 ---p 001c0000 fd:00 42729973 /lib/x86_64-linux-gnu/libc-2.23.so 7f7c4f7a9000-7f7c4f7ad000 r--p 001c0000 fd:00 42729973 /lib/x86_64-linux-gnu/libc-2.23.so 7f7c4f7ad000-7f7c4f7af000 rw-p 001c4000 fd:00 42729973 /lib/x86_64-linux-gnu/libc-2.23.so 7f7c4f7af000-7f7c4f7b3000 rw-p 00000000 00:00 0 7f7c4f7b3000-7f7c4f7ca000 r-xp 00000000 fd:00 42729486 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f7c4f7ca000-7f7c4f9c9000 ---p 00017000 fd:00 42729486 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f7c4f9c9000-7f7c4f9ca000 r--p 00016000 fd:00 42729486 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f7c4f9ca000-7f7c4f9cb000 rw-p 00017000 fd:00 42729486 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f7c4f9cb000-7f7c4fad3000 r-xp 00000000 fd:00 42730014 /lib/x86_64-linux-gnu/libm-2.23.so 7f7c4fad3000-7f7c4fcd2000 ---p 00108000 fd:00 42730014 /lib/x86_64-linux-gnu/libm-2.23.so 7f7c4fcd2000-7f7c4fcd3000 r--p 00107000 fd:00 42730014 /lib/x86_64-linux-gnu/libm-2.23.so 7f7c4fcd3000-7f7c4fcd4000 rw-p 00108000 fd:00 42730014 /lib/x86_64-linux-gnu/libm-2.23.so 7f7c4fcd4000-7f7c4fe50000 r-xp 00000000 fd:00 13898030 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 7f7c4fe50000-7f7c50050000 ---p 0017c000 fd:00 13898030 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 7f7c50050000-7f7c5005a000 r--p 0017c000 fd:00 13898030 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 7f7c5005a000-7f7c5005c000 rw-p 00186000 fd:00 13898030 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 7f7c5005c000-7f7c50060000 rw-p 00000000 00:00 0 7f7c50060000-7f7c50078000 r-xp 00000000 fd:00 42730060 /lib/x86_64-linux-gnu/libpthread-2.23.so 7f7c50078000-7f7c50277000 ---p 00018000 fd:00 42730060 /lib/x86_64-linux-gnu/libpthread-2.23.so 7f7c50277000-7f7c50278000 r--p 00017000 fd:00 42730060 /lib/x86_64-linux-gnu/libpthread-2.23.so 7f7c50278000-7f7c50279000 rw-p 00018000 fd:00 42730060 /lib/x86_64-linux-gnu/libpthread-2.23.so 7f7c50279000-7f7c5027d000 rw-p 00000000 00:00 0 7f7c5027d000-7f7c502a3000 r-xp 00000000 fd:00 42729949 /lib/x86_64-linux-gnu/ld-2.23.so 7f7c50472000-7f7c50478000 rw-p 00000000 00:00 0 7f7c504a1000-7f7c504a2000 rw-p 00000000 00:00 0 7f7c504a2000-7f7c504a3000 r--p 00025000 fd:00 42729949 /lib/x86_64-linux-gnu/ld-2.23.so 7f7c504a3000-7f7c504a4000 rw-p 00026000 fd:00 42729949 /lib/x86_64-linux-gnu/ld-2.23.so 7f7c504a4000-7f7c504a5000 rw-p 00000000 00:00 0 7fffd067f000-7fffd06a0000 rw-p 00000000 00:00 0 [stack] 7fffd0787000-7fffd078a000 r--p 00000000 00:00 0 [vvar] 7fffd078a000-7fffd078c000 r-xp 00000000 00:00 0 [vdso] ffffffffff600000-ffffffffff601000 r-xp 00000000 00:00 0 [vsyscall]
https://stackoverflow.com/questions/4729395/error-free-invalid-next-size-fast
Looks like a memory related error.
/tmp/superspreader_canonicalized_equivalent_0.sk file content: |StateAndPacket| program (|StateAndPacket| state_and_packet) { state_and_packet.pkt_0=state_and_packet.pkt_0; if (state_and_packet.pkt_1==1) {state_and_packet.state_group_0_state_0=state_and_packet.state_group_0_state_0+1; if (state_and_packet.state_group_0_state_0==1000) {state_and_packet.state_group_1_state_0=1; ;} ;}else {if (state_and_packet.pkt_1==2) {state_and_packet.state_group_0_state_0=state_and_packet.state_group_0_state_0-1; } } return state_and_packet; } cmd line and results xiangyug@cyclops:~/chipmunk_experiments$ time iterative_solver /tmp/superspreader_canonicalized_equivalent_0.sk example_alus/nested_ifs.stateful_alu stateless_alus/stateless_alu.j2 4 5 10 --parallel-sketch Iteration #1 Total number of hole bits is 952 Sketch file is superspreader_canonicalized_equivalent_0_nested_ifs_stateless_alu_4_5_codegen_iteration_1.sk Synthesis succeeded with 2 bits, proceeding to verification. Verification failed, use returned counterexamples {'pkt_1': 1, 'pkt_0': 0} {'state_group_1_state_0': 0, 'state_group_0_state_0': 999} Iteration #2 Total number of hole bits is 952 Sketch file is superspreader_canonicalized_equivalent_0_nested_ifs_stateless_alu_4_5_codegen_iteration_2.sk Synthesis succeeded with 2 bits, proceeding to verification. Verification failed, use returned counterexamples {'pkt_1': 2, 'pkt_0': 0} {'state_group_1_state_0': 2, 'state_group_0_state_0': 4} Iteration #3 Total number of hole bits is 952 Sketch file is superspreader_canonicalized_equivalent_0_nested_ifs_stateless_alu_4_5_codegen_iteration_3.sk Error in `/usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis': free(): invalid next size (fast): 0x000000000104f660 ======= Backtrace: ========= /lib/x86_64-linux-gnu/libc.so.6(+0x777e5)[0x7f7c4f4607e5] /lib/x86_64-linux-gnu/libc.so.6(+0x8037a)[0x7f7c4f46937a] /lib/x86_64-linux-gnu/libc.so.6(cfree+0x4c)[0x7f7c4f46d53c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d54d] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40d52c] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x42bb71] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x42e618] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x42f654] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x412dd1] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x40c93b] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x404bac] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf0)[0x7f7c4f409830] /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis[0x405f29] ======= Memory map: ======== 00400000-00563000 r-xp 00000000 fd:00 25432926 /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis 00762000-00763000 r--p 00162000 fd:00 25432926 /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis 00763000-00764000 rw-p 00163000 fd:00 25432926 /usr/local/sketch-1.7.5/sketch-backend/src/SketchSolver/cegis 00764000-00765000 rw-p 00000000 00:00 0 009ee000-04c22000 rw-p 00000000 00:00 0 [heap] 7f7c40000000-7f7c40021000 rw-p 00000000 00:00 0 7f7c40021000-7f7c44000000 ---p 00000000 00:00 0 7f7c48000000-7f7c48021000 rw-p 00000000 00:00 0 7f7c48021000-7f7c4c000000 ---p 00000000 00:00 0 7f7c4ebe8000-7f7c4ebe9000 ---p 00000000 00:00 0 7f7c4ebe9000-7f7c4f3e9000 rw-p 00000000 00:00 0 7f7c4f3e9000-7f7c4f5a9000 r-xp 00000000 fd:00 42729973 /lib/x86_64-linux-gnu/libc-2.23.so 7f7c4f5a9000-7f7c4f7a9000 ---p 001c0000 fd:00 42729973 /lib/x86_64-linux-gnu/libc-2.23.so 7f7c4f7a9000-7f7c4f7ad000 r--p 001c0000 fd:00 42729973 /lib/x86_64-linux-gnu/libc-2.23.so 7f7c4f7ad000-7f7c4f7af000 rw-p 001c4000 fd:00 42729973 /lib/x86_64-linux-gnu/libc-2.23.so 7f7c4f7af000-7f7c4f7b3000 rw-p 00000000 00:00 0 7f7c4f7b3000-7f7c4f7ca000 r-xp 00000000 fd:00 42729486 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f7c4f7ca000-7f7c4f9c9000 ---p 00017000 fd:00 42729486 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f7c4f9c9000-7f7c4f9ca000 r--p 00016000 fd:00 42729486 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f7c4f9ca000-7f7c4f9cb000 rw-p 00017000 fd:00 42729486 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f7c4f9cb000-7f7c4fad3000 r-xp 00000000 fd:00 42730014 /lib/x86_64-linux-gnu/libm-2.23.so 7f7c4fad3000-7f7c4fcd2000 ---p 00108000 fd:00 42730014 /lib/x86_64-linux-gnu/libm-2.23.so 7f7c4fcd2000-7f7c4fcd3000 r--p 00107000 fd:00 42730014 /lib/x86_64-linux-gnu/libm-2.23.so 7f7c4fcd3000-7f7c4fcd4000 rw-p 00108000 fd:00 42730014 /lib/x86_64-linux-gnu/libm-2.23.so 7f7c4fcd4000-7f7c4fe50000 r-xp 00000000 fd:00 13898030 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 7f7c4fe50000-7f7c50050000 ---p 0017c000 fd:00 13898030 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 7f7c50050000-7f7c5005a000 r--p 0017c000 fd:00 13898030 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 7f7c5005a000-7f7c5005c000 rw-p 00186000 fd:00 13898030 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.25 7f7c5005c000-7f7c50060000 rw-p 00000000 00:00 0 7f7c50060000-7f7c50078000 r-xp 00000000 fd:00 42730060 /lib/x86_64-linux-gnu/libpthread-2.23.so 7f7c50078000-7f7c50277000 ---p 00018000 fd:00 42730060 /lib/x86_64-linux-gnu/libpthread-2.23.so 7f7c50277000-7f7c50278000 r--p 00017000 fd:00 42730060 /lib/x86_64-linux-gnu/libpthread-2.23.so 7f7c50278000-7f7c50279000 rw-p 00018000 fd:00 42730060 /lib/x86_64-linux-gnu/libpthread-2.23.so 7f7c50279000-7f7c5027d000 rw-p 00000000 00:00 0 7f7c5027d000-7f7c502a3000 r-xp 00000000 fd:00 42729949 /lib/x86_64-linux-gnu/ld-2.23.so 7f7c50472000-7f7c50478000 rw-p 00000000 00:00 0 7f7c504a1000-7f7c504a2000 rw-p 00000000 00:00 0 7f7c504a2000-7f7c504a3000 r--p 00025000 fd:00 42729949 /lib/x86_64-linux-gnu/ld-2.23.so 7f7c504a3000-7f7c504a4000 rw-p 00026000 fd:00 42729949 /lib/x86_64-linux-gnu/ld-2.23.so 7f7c504a4000-7f7c504a5000 rw-p 00000000 00:00 0 7fffd067f000-7fffd06a0000 rw-p 00000000 00:00 0 [stack] 7fffd0787000-7fffd078a000 r--p 00000000 00:00 0 [vvar] 7fffd078a000-7fffd078c000 r-xp 00000000 00:00 0 [vdso] ffffffffff600000-ffffffffff601000 r-xp 00000000 00:00 0 [vsyscall]