diff --git a/scripts/SV-COMP/cpbench.py b/scripts/SV-COMP/cpbench.py new file mode 100644 index 0000000..9e3cbfa --- /dev/null +++ b/scripts/SV-COMP/cpbench.py @@ -0,0 +1,334 @@ +import os +import shutil + + +def get_source_root_dir(): + return os.path.abspath(os.path.join("..", "..", "sv-benchmarks-fork-marek-trtik", "c")) + + +def get_destination_root_dir(): + return os.path.abspath(os.path.join("..", "..", "sv-benchmarks", "c")) + + +""" + + + +""" + + +def _main(): + for bench_rpath in [ + # "float-benchs/inv_Newton_false-unreach-call.c" + # + # "ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c", + # "ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c", + # "ntdrivers/parport_true-unreach-call.i.cil.c", + # + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--media--usb--s2255--s2255drv.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb--dvb-usb-opera.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--digi_acceleport.ko-entry_point_true-unreach-call.cil.out.c", + # + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--misc--sgi-gru--gru.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--prism54--prism54.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--appletalk--ipddp.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--wireless--prism54--prism54.ko-entry_point_true-unreach-call.cil.out.c", + # + # "ldv-linux-3.4-simple/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--platform--x86--panasonic-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--platform--x86--topstar-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # + # "ldv-commit-tester/main0_true-unreach-call_drivers-media-video-tlg2300-poseidon-ko--32_7a--4a349aa.c", + # "ldv-commit-tester/main3_true-unreach-call_drivers-media-video-tlg2300-poseidon-ko--32_7a--4a349aa-1_false-termination.c", + # "ldv-commit-tester/main3_true-unreach-call_drivers-media-video-tlg2300-poseidon-ko--32_7a--4a349aa_false-termination.c", + # + # "ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--block--paride--pf.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--batman-adv--batman-adv.ko-ldv_main15_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--block--paride--pcd.ko-main.cil.out.c", + # "ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--block--paride--pf.ko-main.cil.out.c", + # + # "list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i", + # "ldv-memsafety/memset2_false-valid-deref-write.c", + # "ldv-memsafety/memset3_false-valid-deref-write.c", + # "ldv-memsafety/memsetNonZero2_false-valid-deref-write.c", + # "ldv-memsafety/memsetNonZero3_false-valid-deref-write.c", + # "ldv-memsafety/memsetNonZero_false-valid-deref-write.c", + # "ldv-memsafety/memset_false-valid-deref-write.c", + # "ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety.i", + # "ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i", + # "ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i", + # "ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i", + # + # "ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i", + # "busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i", + # "busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i", + # + # "ldv-races/race-4_1-thread_local_vars_true-unreach-call.i", + # + # "heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i", + # "heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i", + # "ntdrivers/cdaudio_false-unreach-call.i.cil.c", + # "ntdrivers/cdaudio_true-unreach-call.i.cil.c", + # "ldv-sets/test_add_false-unreach-call_true-termination.i", + # "ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i", + # "ldv-sets/test_mutex_double_unlock_false-unreach-call.i", + # "ldv-sets/test_mutex_unbounded_false-unreach-call.i", + # "memsafety/test-0137_false-valid-deref.i", + # "ldv-sets/test_add_false-unreach-call_true-termination.i", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--device_handler--scsi_dh_rdac.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--libertas--libertas.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--mtd--ubi--ubi.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--scsi--st.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--megaraid--megaraid_mm.ko-entry_point_false-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--input--mousedev.ko-entry_point_false-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--gpu--drm--mgag200--mgag200.ko-entry_point_false-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c", + # "ldv-validator-v0.8/linux-stable-063f96c-1-144_2a-drivers--mmc--host--vub300.ko.unsigned-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c", + # + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--bluetooth--hci_uart.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--power--bq2415x_charger.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--scsi--sg.ko-entry_point_false-unreach-call.cil.out.c", + # "ldv-validator-v0.8/linux-stable-4a349aa-1-32_7a-drivers--media--video--tlg2300--poseidon.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c", + # "ldv-validator-v0.8/linux-stable-064368f-1-111_1a-drivers--media--radio--si4713-i2c.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c", + # + # "loop-industry-pattern/ofuf_1_true-unreach-call.c", + # "loop-industry-pattern/ofuf_1_true-unreach-call.c", + # "loop-industry-pattern/ofuf_2_true-unreach-call.c", + # "loop-industry-pattern/ofuf_3_true-unreach-call.c", + # "loop-industry-pattern/ofuf_4_true-unreach-call.c", + # "loop-industry-pattern/ofuf_5_true-unreach-call.c", + # + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--atheros--alx--alx.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--intel--ixgb--ixgb.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--marvell--skge.ko-entry_point_true-unreach-call.cil.out.c", + # + # "ldv-linux-3.4-simple/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb--dvb-usb-opera.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--media--usb--s2255--s2255drv.ko-entry_point_true-unreach-call.cil.out.c", + # "ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--digi_acceleport.ko-entry_point_true-unreach-call.cil.out.c", + # + # "ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i", + # "ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i", + # + # "termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c", + # "termination-restricted-15/Ex05_false-termination_true-no-overflow.c", + # + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-freecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-jumpshot.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6027.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--dmx3191d.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # + # "ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c", + # + # "ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mouse--synaptics_usb_false-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--cpia2--cpia2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--wireless--p54--p54usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c", + # + # "ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--ad714x-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--zio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c", + # + # "pthread-wmm/mix000_power.oepc_false-unreach-call.i", # OK! + # "pthread-wmm/mix000_power.opt_false-unreach-call.i", # OK! + # "pthread-wmm/mix008_power.oepc_false-unreach-call.i", + # "pthread-wmm/mix031_pso.oepc_false-unreach-call.i", + # "pthread-wmm/thin000_rmo.opt_false-unreach-call.i", + # "pthread-wmm/rfi008_tso.opt_false-unreach-call.i", # OK! + # + # "pthread-lit/fkp2013_variant_false-unreach-call.i", # PROBLEM! Verification result: UNKNOWN, incomplete analysis. + # "pthread-lit/qw2004_false-unreach-call.i", + # + # "ldv-races/race-1_3-join_false-unreach-call.i", # OK! + # "ldv-races/race-4_2-thread_local_vars_false-unreach-call.i", + # + # "pthread-driver-races/char_generic_nvram_read_nvram_write_nvram_false-unreach-call.i", # OK! + # "pthread-driver-races/char_pc8736x_gpio_pc8736x_gpio_change_pc8736x_gpio_current_false-unreach-call.i", + # "pthread-driver-races/char_pc8736x_gpio_pc8736x_gpio_change_pc8736x_gpio_set_false-unreach-call.i", + # "pthread-driver-races/char_pc8736x_gpio_pc8736x_gpio_current_pc8736x_gpio_set_false-unreach-call.i", + # + # "pthread-C-DAC/pthread-demo-datarace_false-unreach-call.i", # OK! + # + # "pthread/lazy01_false-unreach-call.i", # OK! + # "pthread/fib_bench_false-unreach-call.i", + # "pthread/fib_bench_longer_false-unreach-call.i", + # "pthread/fib_bench_longest_false-unreach-call.i", + # "pthread/queue_longer_false-unreach-call.i", + # "pthread/queue_longest_false-unreach-call.i", + # + # "pthread/stack_false-unreach-call.i", # PROBLEM! Verification result: UNKNOWN, incomplete analysis. Error: Unsupported C feature (BDD-analysis does not support arrays: stack[__CPAchecker_TMP_1]) (BDDVectorCExpressionVisitor.visit, SEVERE) + # "pthread/stateful01_false-unreach-call.i", + # "pthread/stack_longer_false-unreach-call.i", + # "pthread/stack_longest_false-unreach-call.i", + # + # "pthread-atomic/qrcu_false-unreach-call.i", # OK! + # "pthread-atomic/read_write_lock_false-unreach-call.i", + # + # "pthread-ext/28_buggy_simple_loop1_vf_false-unreach-call.i", # PROBLEM! Verification result: UNKNOWN, incomplete analysis. Error: Unrecognized code (multiple thread assignments to same LHS not supported: t) (ThreadingTransferRelation.getNewThreadId, SEVERE) + # "pthread-ext/27_Boop_simple_vf_false-unreach-call.i", + # "pthread-ext/32_pthread5_vs_false-unreach-call.i", + # "pthread-ext/25_stack_longer_false-unreach-call.i", + # "pthread-ext/26_stack_cas_longest_false-unreach-call.i", + # + # "pthread-wmm/safe036_power.opt_true-unreach-call.i", # PROBLEM! Verification result: UNKNOWN, incomplete analysis. Error: line 728: Unsupported feature (pthread_create): pthread_create(&t2629, (void *)0, &P0, (void *)0); (line was originally pthread_create(&t2629, ((void *)0), P0, ((void *)0));) (CallstackTransferRelation.getAbstractSuccessorsForEdge, SEVERE) + # "pthread-driver-races/char_pc8736x_gpio_pc8736x_gpio_change_pc8736x_gpio_configure_true-unreach-call.i", + # "pthread-wmm/safe000_pso.opt_true-unreach-call.i", + # + # "ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--ad714x-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--mma8450.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--mpu3050.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--touchscreen--eeti_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--touchscreen--max11801_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--leds--leds-pca9633.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-cinergyT2.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dtt200u.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-mxl111sf.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-vp7045.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--net--usb--cdc_subset.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--net--usb--plusb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--iio--addac--adt7316-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--iio--meter--ade7854-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--serqt_usb2--serqt_usb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--dwc3--dwc3-pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--misc--trancevibrator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--cp210x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--empeg.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--funsoft.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--hp4x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--ipw.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--mos7840.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--moto_modem.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--qcaux.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--siemens_mpi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--ssu100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--usb_debug.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--vivopay-serial.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--zio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mouse--synaptics_usb_false-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--cpia2--cpia2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--wireless--p54--p54usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c", + # "ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c", + # + # "pthread/bigshot_p_false-unreach-call.i", + # "busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i", + # "array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i", + # "array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i", + # "array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i", + # "pthread-wmm/mix003_tso.oepc_false-unreach-call.i", + # "pthread-wmm/mix006_pso.opt_false-unreach-call.i", + # "pthread-wmm/mix009_tso.opt_false-unreach-call.i", + # + # "busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i", + # + # "array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i", + # "array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i", + # "array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i", + # + # "memsafety/test-0504_true-valid-memsafety.i", + # "memsafety-ext/dll_extends_pointer_true-valid-memsafety.i", + # "memsafety-ext2/length_test03_false-valid-memtrack.i", + # "list-ext-properties/test-0513_1_true-valid-memsafety.i", + # + # "ldv-memsafety/memleaks_test19_false-valid-free.i", + # "ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i", + # "ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i", + # "forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i", + # "forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i", + # + # "floats-esbmc-regression/floor_nondet_true-unreach-call.i", + # "floats-esbmc-regression/isgreater_true-unreach-call.i", + # "floats-esbmc-regression/round_nondet_true-unreach-call.i", + # + # "forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i", + # "list-ext2-properties/simple_search_value_true-unreach-call.i", + # "ldv-sets/test_add_true-unreach-call_true-termination.i", + # + # "loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i", + # + # "busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i", + # "busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i", + # + # "busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i", + # "busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i", + + # "pthread-C-DAC/pthread-demo-datarace_false-unreach-call.i", + "pthread-complex/bounded_buffer_false-unreach-call.i", + + ]: + if True: # Copy from repo to local evaluation dir + os.makedirs(os.path.dirname(os.path.join(get_destination_root_dir(), bench_rpath)), exist_ok=True) + shutil.copy(os.path.join(get_source_root_dir(), bench_rpath), os.path.join(get_destination_root_dir(), bench_rpath)) + else: # Copy back from local evaluation dir to repo + shutil.copy(os.path.join(get_destination_root_dir(), bench_rpath), os.path.join(get_source_root_dir(), bench_rpath)) + + +if __name__ == "__main__": + exit(_main()) diff --git a/scripts/SV-COMP/evalall.py b/scripts/SV-COMP/evalall.py new file mode 100755 index 0000000..acf618f --- /dev/null +++ b/scripts/SV-COMP/evalall.py @@ -0,0 +1,61 @@ +import os +import shutil +import subprocess +import time + + +def get_benchmarks(): + return [ + "ntdrivers/floppy2_true-unreach-call.i.cil.c", + ] + + +def run_tool(command_to_execute, current_working_dir, timeout_in_seconds): + start_time = time.time() + process = subprocess.Popen( + command_to_execute, + cwd=current_working_dir, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + shell=True, + preexec_fn=os.setsid + ) + while time.time() - start_time < timeout_in_seconds: + is_allive = process.poll() + if is_allive is not None: + return True, str(process.stdout.read()) + str(process.stderr.read()) + time.sleep(0.005) + try: + os.killpg(os.getpgid(process.pid), subprocess.signal.SIGTERM) + except ProcessLookupError: + if process.poll(): + print(" WARNING: failed to kill the process! (PID=" + str(process.pid) + ")") + return False, "" + + +def _main(): + outdir = "./evalall_results" + os.makedirs(outdir, exist_ok=True) + for benchmark in get_benchmarks(): + print("Processing " + benchmark) + # stime = time.time() + # out, err = subprocess.Popen(["python3", "./evaluate.py", benchmark], stdout=subprocess.PIPE, stderr=subprocess.PIPE).communicate() + # etime = time.time() + # sss = etime - stime + # print("Time = " + str(sss)) + # output = out.decode("utf-8") + err.decode("utf-8") + + state, output = run_tool("./evalall.sh \"" + benchmark + "\"", os.getcwd(), 3 * 60) + if state is False: + output = "EXECUTION OF THE TOOL FAILED!\n\n\n" + output + print(output) + + with open(os.path.join(outdir, os.path.basename(benchmark) + ".txt"), "w") as ofile: + ofile.write(output) + shutil.copy("./witness", os.path.join(outdir, os.path.basename(benchmark) + ".xml")) + print("\n\n\n") + return 0 + + +if __name__ == "__main__": + exit(_main()) diff --git a/scripts/SV-COMP/evaluate.py b/scripts/SV-COMP/evaluate.py new file mode 100755 index 0000000..3ece185 --- /dev/null +++ b/scripts/SV-COMP/evaluate.py @@ -0,0 +1,212 @@ +import os +import sys +import traceback +import shutil +import argparse +import json +import re + + +def _get_this_script_dir(): + return os.path.dirname(__file__) + + +def _get_cbmc_new_repo_dir(): + return os.path.abspath(os.path.join(_get_this_script_dir(), "cbmc-fork-marek-trtik")) + + +def _get_cbmc_new_binary(): + return os.path.abspath(os.path.join(_get_cbmc_new_repo_dir(), "src", "cbmc", "cbmc")) + + +def _get_installed_cbmc_new_binary(): + return os.path.abspath(os.path.join(_get_this_script_dir(), "cbmc-sv-comp-2017-pr-rebase-binary")) + + +def _get_cbmc_new_shell_script(): + return _get_installed_cbmc_new_binary()[:_get_installed_cbmc_new_binary().rfind("-binary")] + + +def _get_cbmc_old_repo_dir(): + return os.path.abspath(os.path.join(_get_this_script_dir(), "cbmc-fork-tautschnig")) + + +def _get_cbmc_old_binary(): + return os.path.abspath(os.path.join(_get_cbmc_old_repo_dir(), "src", "cbmc", "cbmc")) + + +def _get_installed_cbmc_old_binary(): + return os.path.abspath(os.path.join(_get_this_script_dir(), "cbmc-sv-comp-2017-pr-binary")) + + +def _get_cbmc_old_shell_script(): + return _get_installed_cbmc_old_binary()[:_get_installed_cbmc_old_binary().rfind("-binary")] + + +def _get_benchmarks_root_dir(): + return os.path.abspath(os.path.join(_get_this_script_dir(), "..", "sv-benchmarks", "c")) + + +def _get_results_diff_json_pathname(): + return os.path.abspath(os.path.join(_get_this_script_dir(), "..", "RESULTS", "diff_CBMC-sv-comp-2017-pr-rebase_CBMC-sv-comp-2017-pr.json")) + + +def _build_command_line_interface(): + parser = argparse.ArgumentParser( + description="TODO", + ) + parser.add_argument("-V", "--version", action="store_true", + help="Prints the version string of the module.") + parser.add_argument( + "benchmark", type=str, + help="TODO") + parser.add_argument( + "--old-cbmc", action="store_true", + help="TODO" + ) + cmdline = parser.parse_args() + + if cmdline.version: + print("v.1.0") + exit(0) + + if not os.path.isfile(cmdline.benchmark): + if not os.path.isfile(os.path.join(_get_benchmarks_root_dir(), cmdline.benchmark)): + print("ERROR: In option 'benchmark': The passed path does not reference an existing file.") + exit(1) + else: + cmdline.benchmark = os.path.join(_get_benchmarks_root_dir(), cmdline.benchmark) + cmdline.benchmark = os.path.abspath(cmdline.benchmark) + + return cmdline + + +""" +def get_cbmc_command_line_options(): + return "--graphml-witness witness.graphml --32 --propertyfile ../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/eca-rers2012/Problem01_label00_true-unreach-call.c + "--graphml-witness $LOG.witness --unwind $c --stop-on-fail $BIT_WIDTH $PROPERTY --function $ENTRY $BM" + +* executing the following command: + grep "^bitvector/.*unreach-call" *.set + in '../sv-benchmarks/c' produces: + ReachSafety-BitVectors.set:bitvector/*_false-unreach-call*.i + ReachSafety-BitVectors.set:bitvector/*_true-unreach-call*.i + ReachSafety-BitVectors.set:bitvector/*_false-unreach-call*.BV.c.cil.c + ReachSafety-BitVectors.set:bitvector/*_true-unreach-call*.c.cil.c + where I found the strings "bitvector" and "unreach-call" in the JSON file: + ========== This is the string + "better_right": { v + "../../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i": { + "category": "unreach-call", + "left_status": "ERROR (42)", + "left_status_value": 2, + "options": "--32", <======= This is the option for the shell script + "properties": "unreach-call", <======= This is the string + "right_status": "true", + "right_status_value": 1 + }, + + I should thus call the shell script: + /home/marek/root/SV-COMP-2018/BUG_FIXING/cbmc-sv-comp-2017-pr-rebase + with these options + ./cbmc-sv-comp-2017-pr-rebase --graphml-witness witness.graphml ${options} --propertyfile ${propertyfile} ${benchmark} + where + ${options}=--32 (this was taken from the JSON file, see above) + ${propertyfile}=../sv-benchmarks/c/ReachSafety.prp (this was obtained from the result of the grep command) + ${benchmark}=../sv-benchmarks/c/eca-rers2012/Problem01_label00_true-unreach-call.c (this was taken from the JSON file, see above) + +""" + + +def _install_cbmc(use_old_cbmc): + repo_dir = _get_cbmc_old_repo_dir() if use_old_cbmc else _get_cbmc_new_repo_dir() + cbmc_binary = _get_cbmc_old_binary() if use_old_cbmc else _get_cbmc_new_binary() + cbmc_installed_binary = _get_installed_cbmc_old_binary() if use_old_cbmc else _get_installed_cbmc_new_binary() + if os.path.isfile(cbmc_installed_binary): + os.remove(cbmc_installed_binary) + old_cwd = os.getcwd() + os.chdir(repo_dir) + command = "make -C src" + print("EXECUTING: IN[" + repo_dir + "]: " + command) + retval = os.system(command) + os.chdir(old_cwd) + if retval != 0: + print("ERROR: execution of the last shell command has FAILED.") + return retval + shutil.copy(cbmc_binary, cbmc_installed_binary) + return 0 + + +def _load_diff_record_of_benchmark(benchmark_pathname): + with open(_get_results_diff_json_pathname(), "r") as ifile: + diff = json.loads(ifile.read()) + assert "better_right" in diff + record_name = os.path.relpath(benchmark_pathname, _get_benchmarks_root_dir()) + assert record_name in diff["better_right"] + record = diff["better_right"][record_name] + return record + + +def _get_property_file(benchmark_pathname, raw_benchmark_category): + benchmark_dirname = os.path.dirname(os.path.relpath(benchmark_pathname, _get_benchmarks_root_dir())) + benchmark_category = raw_benchmark_category if raw_benchmark_category != "valid-memtrack" else "valid-memsafety" + for pathname in [os.path.abspath(os.path.join(_get_benchmarks_root_dir(), fname)) + for fname in os.listdir(_get_benchmarks_root_dir()) + if os.path.splitext(fname)[1] == ".set"]: + with open(pathname, "r") as ifile: + content = ifile.read() + if re.findall("^" + benchmark_dirname + "/.*" + benchmark_category, content, re.MULTILINE): + property_file_pathname = os.path.splitext(pathname)[0] + ".prp" + if os.path.isfile(property_file_pathname): + return property_file_pathname + property_file_pathname_ex = os.path.join( + os.path.dirname(pathname), + os.path.basename(pathname)[:os.path.basename(pathname).find("-")] + ".prp" + ) + if os.path.isfile(property_file_pathname_ex): + return property_file_pathname_ex + print("ERROR: the property file " + property_file_pathname + " of the found corresponding file " + + pathname + " does not exist. Skipping the file.") + print("ERROR: the property file " + property_file_pathname_ex + " of the found corresponding file " + + pathname + " does not exist. Skipping the file.") + print("ERROR: cannot find any property file (*.set) for the benchmark " + benchmark_pathname + + " and the category " + benchmark_category) + assert False + + +def _evaluate_benchmark(benchmark_pathname, use_old_cbmc): + assert isinstance(benchmark_pathname, str) + assert isinstance(use_old_cbmc, bool) + + retval = _install_cbmc(use_old_cbmc) + if retval != 0: + return retval + record = _load_diff_record_of_benchmark(benchmark_pathname) + cbmc_script = _get_cbmc_old_shell_script() if use_old_cbmc else _get_cbmc_new_shell_script() + property_file = _get_property_file(benchmark_pathname, record["category"]) + + command = ( + cbmc_script + " " + + "--graphml-witness witness witness.graphml " + + "--propertyfile " + property_file + " " + + record["options"] + " " + + benchmark_pathname + ) + print("EXECUTING: IN[" + os.getcwd() + "]: " + command) + return os.system(command) + + +def _main(cmdline): + retval = 0 + try: + retval = _evaluate_benchmark(cmdline.benchmark, cmdline.old_cbmc) + except: + print("ERROR: An exception was raised:") + traceback.print_exc(file=sys.stdout) + retval = 2 + finally: + return retval + + +if __name__ == "__main__": + exit(_main(_build_command_line_interface())) diff --git a/scripts/SV-COMP/mkxmlparts.py b/scripts/SV-COMP/mkxmlparts.py new file mode 100644 index 0000000..17f4844 --- /dev/null +++ b/scripts/SV-COMP/mkxmlparts.py @@ -0,0 +1,50 @@ +import os +import shutil + + +def get_num_parts(): + return 23 + + +def get_source_file(): + return os.path.abspath("cbmc.xml") + + +def get_destination_file(idx): + src_file = get_source_file() + dir_name = os.path.dirname(src_file) + file_name = os.path.basename(src_file) + plain_file_name, extension = os.path.splitext(file_name) + return os.path.join(dir_name, plain_file_name + str(idx) + extension) + + +def update_part_file(idx): + assert idx > 0 + with open(get_destination_file(idx), "r") as ifile: + content = ifile.read() + first_task_idx = content.find(" 0 + + my_task_idx = 0 + for i in range(idx): + my_task_idx = content.find(" 0 + my_task_end_idx = content.find("", my_task_idx) + assert my_task_end_idx > my_task_idx + my_task_end_idx += len("") + + tasks_end_idx = content.rfind("") + assert tasks_end_idx > my_task_end_idx + + with open(get_destination_file(idx), "w") as ofile: + ofile.write(content[:first_task_idx] + content[my_task_idx:my_task_end_idx] + "\n\n" + content[tasks_end_idx:]) + + +def _main(): + for i in range(1, get_num_parts() + 1): + shutil.copy(get_source_file(), get_destination_file(i)) + update_part_file(i) + + +if __name__ == "__main__": + exit(_main()) diff --git a/scripts/SV-COMP/results_download.py b/scripts/SV-COMP/results_download.py new file mode 100755 index 0000000..6c8ee44 --- /dev/null +++ b/scripts/SV-COMP/results_download.py @@ -0,0 +1,40 @@ +import os + + +for name, ip in [ + ("sv-comp-cbmc-incremental-ele-part1", "35.195.26.50"), + ("sv-comp-cbmc-incremental-ele-part2", "35.195.8.91"), + ("sv-comp-cbmc-incremental-part1", "35.195.116.95"), + ("sv-comp-cbmc-incremental-part2", "104.199.93.208"), + ("sv-comp-cbmc-incremental-rebase-ele-part1", "35.189.240.44"), + ("sv-comp-cbmc-incremental-rebase-ele-part2", "104.155.32.99"), + ("sv-comp-cbmc-incremental-rebase-part1", "35.187.83.211"), + ("sv-comp-cbmc-incremental-rebase-part2", "104.199.79.254"), + ("sv-comp-cbmc-part1", "35.195.222.120"), + ("sv-comp-cbmc-part2", "192.158.29.5"), + ("sv-comp-cbmc-sv-comp-2017-pr-part1", "35.195.150.6"), + ("sv-comp-cbmc-sv-comp-2017-pr-part2", "35.195.99.239"), + ("sv-comp-cbmc-sv-comp-2017-pr-rebase-part1", "104.199.17.173"), + ("sv-comp-cbmc-sv-comp-2017-pr-rebase-part2", "35.195.208.163"), + ("sv-comp-cbmc-symex-part1", "35.195.185.16"), + ("sv-comp-cbmc-symex-part2", "35.195.42.83") + ]: + user_name = "marek_trtik" + dst_dir = os.path.join( + "RESULTS", + "NOW", + name[len("sv-comp-"):min(name.rfind("-ele") if "-ele" in name else len(name), + name.rfind("-part") if "-part" in name else len(name))], + "results" + ) + os.makedirs(dst_dir, exist_ok=True) + command_prefix = "scp " + user_name + "@" + ip + ":" + "~/evaluation-root/results/*." + command_suffix = " " + dst_dir + print("Retrieving results for " + name + " from " + ip) + # print("Executing: " + command) + retval = os.system(command_prefix + "bz2" + command_suffix) + if retval != 0: + retval = os.system(command_prefix + "xml" + command_suffix) + if retval != 0: + print(" ERROR: The download has failed!") + diff --git a/scripts/SV-COMP/run.py b/scripts/SV-COMP/run.py new file mode 100755 index 0000000..43da83d --- /dev/null +++ b/scripts/SV-COMP/run.py @@ -0,0 +1,143 @@ +import argparse +import shutil +import os +import json + + +def _get_my_dir(): return os.path.dirname(os.path.realpath(__file__)) + + +def _parse_cmd_line(): + parser = argparse.ArgumentParser( + description="The script automates the installation, removeal, and evalaution of individual versions " + " of CBMC in the 'benchexec' framework.") + parser.add_argument("-V", "--version", action="store_true", + help="Prints a version string.") + parser.add_argument("--install", type=str, + help="To add (install) a tool into 'benchexec'.") + parser.add_argument("--remove", type=str, + help="To remove (uninstall) a tool from 'benchexec'.") + parser.add_argument("--evaluate", type=str, + help="To start the evaluation.") + parser.add_argument("--part", type=int, + help="A number of an XML file to be used.") + parser.add_argument("--timeout", type=int, + help="Number of seconds reserved for analysis.") + parser.add_argument("--tasks", nargs='+', + help="A list of verifications task to be performed " + "(a subset of tasks specied in the XML file).") + return parser.parse_args() + + +def get_names_of_tools(): + return { + "cbmc", + "cbmc-incremental", + "cbmc-incremental-ele", + "cbmc-incremental-rebase", + "cbmc-incremental-rebase-ele", + "cbmc-sv-comp-2017-pr", + "cbmc-sv-comp-2017-pr-rebase", + "cbmc-symex", + "xtest" + } + + +def get_install_directories_of_tools(): + return {name: os.path.join( + _get_my_dir(), + "..", + "cbmc-versions", + name if not name.endswith("-ele") else name[:-4], + "bin" + ) + for name in get_names_of_tools()} + + +def clean_old_results(): + if os.path.isdir(os.path.join(_get_my_dir(), "results")): + print("sudo rm -rf \"" + os.path.join(_get_my_dir(), "results") + "\"") + os.system("sudo rm -rf \"" + os.path.join(_get_my_dir(), "results") + "\"") + if os.path.isfile(os.path.join(_get_my_dir(), "witness.graphml")): + print("sudo rm -f \"" + os.path.join(_get_my_dir(), "witness.graphml") + "\"") + os.system("sudo rm -f \"" + os.path.join(_get_my_dir(), "witness.graphml") + "\"") + + +def install_tool(tool_name, xml_part, benchexec_tools_path): + assert tool_name in get_names_of_tools() + os.system("sudo cp \"" + os.path.join(get_install_directories_of_tools()[tool_name], tool_name + ".py") + + "\" \"" + os.path.join(benchexec_tools_path, tool_name + ".py") + "\"") + shutil.copy(os.path.join(get_install_directories_of_tools()[tool_name], tool_name), + os.path.join(_get_my_dir(), tool_name)) + shutil.copy(os.path.join(get_install_directories_of_tools()[tool_name], tool_name + "-binary"), + os.path.join(_get_my_dir(), tool_name + "-binary")) + xml_part_name = "" if xml_part is None else str(xml_part) + shutil.copy(os.path.join(get_install_directories_of_tools()[tool_name], tool_name + xml_part_name + ".xml"), + os.path.join(_get_my_dir(), tool_name + xml_part_name + ".xml")) + + +def remove_tool(tool_name, xml_part, benchexec_tools_path): + assert tool_name in get_names_of_tools() + os.system("sudo rm -f \"" + os.path.join(benchexec_tools_path, tool_name + ".py") + "\"") + os.remove(os.path.join(_get_my_dir(), tool_name)) + os.remove(os.path.join(_get_my_dir(), tool_name + "-binary")) + xml_part_name = "" if xml_part is None else str(xml_part) + os.remove(os.path.join(_get_my_dir(), tool_name + xml_part_name + ".xml")) + + +def evaluate_tool(tool_name, xml_part, timeout_seconds, tasks): + assert tool_name in get_names_of_tools() + clean_old_results() + os.system("sudo swapoff -a") + xml_part_name = "" if xml_part is None else str(xml_part) + timeout_string = (" -T " + str(timeout_seconds) + "s ") if timeout_seconds is not None else "" + tasks = (" --tasks " + " ".join(tasks)) if tasks is not None and isinstance(tasks, list) and len(tasks) > 0 else "" + os.system( + "sudo benchexec --no-container " + + timeout_string + + tool_name + xml_part_name + ".xml " + + tasks + ) + + +def _main(): + cmdline = _parse_cmd_line() + + if cmdline.version: + print("v.1.0") + return + + benchexec_tools_path_json = os.path.join(_get_my_dir(), "benchexec_tools_path.json") + if not os.path.isfile(benchexec_tools_path_json): + default_benchexec_tools_path = "/usr/local/lib/python3.5/dist-packages/benchexec/tools" + if os.path.isdir(default_benchexec_tools_path): + benchexec_tools_path = default_benchexec_tools_path + else: + benchexec_tools_path = None + for root, dir_names, _ in os.walk("/"): + if root.endswith("/benchexec/tools"): + benchexec_tools_path = root + break + if benchexec_tools_path is None: + print("ERROR: Cannot find the benchexec's install dir 'dist-packages/benchexec/tools' for tools.") + return -1 + with open(benchexec_tools_path_json, "w") as ofile: + ofile.write(json.dumps({"benchexec_tools_path": benchexec_tools_path}, sort_keys=True, indent=4)) + with open(benchexec_tools_path_json, "r") as ifile: + benchexec_tools_path = json.load(ifile)["benchexec_tools_path"] + + if cmdline.install is not None: + install_tool(cmdline.install, cmdline.part, benchexec_tools_path) + + if cmdline.remove is not None: + remove_tool(cmdline.remove, cmdline.part, benchexec_tools_path) + + if cmdline.evaluate is not None: + evaluate_tool(cmdline.evaluate, cmdline.part, cmdline.timeout, cmdline.tasks) + + return 0 + + +if __name__ == "__main__": + exit(_main()) + diff --git a/scripts/SV-COMP/searchfiles.py b/scripts/SV-COMP/searchfiles.py new file mode 100644 index 0000000..1f0e1e8 --- /dev/null +++ b/scripts/SV-COMP/searchfiles.py @@ -0,0 +1,163 @@ +import os +import argparse +import json +import re + + +def _build_command_line_interface(): + parser = argparse.ArgumentParser( + description="TODO", + ) + parser.add_argument("-V", "--version", action="store_true", + help="Prints the version string of the module.") + parser.add_argument( + "input", type=str, + help="TODO") + parser.add_argument( + "output", type=str, + help="TODO" + ) + cmdline = parser.parse_args() + + if cmdline.version: + print("v.1.0") + exit(0) + + if not os.path.isdir(cmdline.input): + print("ERROR: In option 'input': The passed input directory does not exist.") + exit(1) + if os.path.isdir(cmdline.output): + print("ERROR: In option 'output': The passed output file is an existing directory.") + exit(1) + if os.path.splitext(cmdline.output)[1].lower() != ".json": + print("ERROR: In option 'input': The passed output file does not have '.json' extension.") + exit(1) + + return cmdline + + +def search_benchmarks_for_fopen_and_FILE(cmdline): + + def is_desired(content): + if "fopen" in content: + return True + for candidate in [" FILE ", "\tFILE ", " FILE\t", "\tFILE\t", " FILE*", "\tFILE*"]: + if candidate in content: + return True + return False + + result = [] + for fdir, fname in [(os.path.abspath(dirpath), fname) + for dirpath, _, filenames in os.walk(cmdline.input) + for fname in filenames + if not dirpath.lower().endswith("-todo") and + os.path.splitext(fname)[1].lower() in [".c", ".i"]]: + pathname = os.path.join(fdir, fname) + with open(pathname, "r") as ifile: + content = ifile.read() + if is_desired(content): + result.append(pathname) + ifiles = [fname for fname in result if fname.endswith(".i")] + cfiles = [fname for fname in result if fname.endswith(".c") and fname[:-2]+".i" not in ifiles] + os.makedirs(os.path.dirname(cmdline.output), exist_ok=True) + with open(cmdline.output, "w") as ofile: + ofile.write(json.dumps(ifiles + cfiles, sort_keys=True, indent=4)) + + +def search_logs_for_message(cmdline, message, category=None): + falsification = [] + result = [] + num_log_files = 0 + for fdir, fname in [(os.path.abspath(dirpath), fname) + for dirpath, _, filenames in os.walk(cmdline.input) + for fname in filenames + if os.path.splitext(fname)[1].lower() == ".log"]: + num_log_files += 1 + pathname = os.path.join(fdir, fname) + with open(pathname, "r") as ifile: + content = ifile.read() + if message in content: + benchmark = None + matches = re.findall("^Parsing .*$", content, re.MULTILINE) + if len(matches) == 1: + raw_pathname = matches[0][8:] + benchmark = os.path.join(os.path.basename(os.path.dirname(raw_pathname)), os.path.basename(raw_pathname)) + result.append({pathname: benchmark}) + if "_false-" + ("" if category is None else category) in benchmark: + falsification.append(benchmark) + os.makedirs(os.path.dirname(cmdline.output), exist_ok=True) + with open(cmdline.output, "w") as ofile: + ofile.write(json.dumps({"issues": result, "falsification": sorted(falsification)}, sort_keys=True, indent=4)) + print("There was searched " + str(num_log_files) + " files.") + + +def search_logs_for_errors(cmdline): + result = dict() + num_log_files = 0 + for fdir, fname in [(os.path.abspath(dirpath), fname) + for dirpath, _, filenames in os.walk(cmdline.input) + for fname in filenames + if os.path.splitext(fname)[1].lower() == ".log"]: + num_log_files += 1 + pathname = os.path.join(fdir, fname) + with open(pathname, "r") as ifile: + lines = ifile.readlines() + + keys = [] + for i in reversed(range(len(lines))): + line = lines[i].strip() + if len(line) == 0: + continue + keys.append(line) + if len(keys) == 3: + break + if len(keys) == 0: + key = "" + else: + key = "::".join(keys) + + benchmark = None + for i in range(len(lines)): + line = lines[i].strip() + matches = re.findall("^Parsing .*$", line) + if len(matches) == 1: + raw_pathname = matches[0][8:] + benchmark = os.path.join(os.path.basename(os.path.dirname(raw_pathname)), + os.path.basename(raw_pathname)) + break + if benchmark is None: + benchmark = "UNKNOWN [log='" + pathname + "']" + key = "" + + if key in result: + result[key].append(benchmark) + else: + result[key] = [benchmark] + + sorted_result = {key: sorted(benchmarks) for key, benchmarks in result.items()} + statistics = dict() + for key, benchmarks in result.items(): + statistics[key] = len(benchmarks) + + os.makedirs(os.path.dirname(cmdline.output), exist_ok=True) + with open(cmdline.output, "w") as ofile: + ofile.write(json.dumps({"results": sorted_result, "statistics": statistics}, sort_keys=True, indent=4)) + print("There was searched " + str(num_log_files) + " files.") + + +def _main(cmdline): + # search_benchmarks_for_fopen_and_FILE(cmdline) + # search_logs_for_message(cmdline, "implicit conversion not permitted", "unreach-call") + # search_logs_for_message(cmdline, "cannot unpack struct with non-byte aligned components:") + # search_logs_for_message(cmdline, "byte_update of unknown width:") + # search_logs_for_message(cmdline, "equality without matching types") + # search_logs_for_message(cmdline, "={ [") + # search_logs_for_message(cmdline, "terminate called after throwing an instance of 'int'") + search_logs_for_message(cmdline, "Numeric exception :") + # search_logs_for_errors(cmdline) + + + + +if __name__ == "__main__": + exit(_main(_build_command_line_interface())) diff --git a/scripts/SV-COMP/setcollect.py b/scripts/SV-COMP/setcollect.py new file mode 100644 index 0000000..246a95d --- /dev/null +++ b/scripts/SV-COMP/setcollect.py @@ -0,0 +1,65 @@ +import os +import argparse +import glob +import json + + +def _build_command_line_interface(): + parser = argparse.ArgumentParser( + description="TODO", + ) + parser.add_argument("-V", "--version", action="store_true", + help="Prints the version string of the module.") + parser.add_argument( + "input", type=str, + help="TODO") + parser.add_argument( + "output", type=str, + help="TODO" + ) + cmdline = parser.parse_args() + + if cmdline.version: + print("v.1.0") + exit(0) + + if not os.path.isfile(cmdline.input): + print("ERROR: In option 'input': The passed input file does not exist.") + exit(1) + if os.path.splitext(cmdline.input)[1].lower() != ".set": + print("ERROR: In option 'input': The passed output file does not have '.set' extension.") + exit(1) + if os.path.isdir(cmdline.output): + print("ERROR: In option 'output': The passed output file is an existing directory.") + exit(1) + if os.path.splitext(cmdline.output)[1].lower() != ".json": + print("ERROR: In option 'input': The passed output file does not have '.json' extension.") + exit(1) + + return cmdline + + +def _main(cmdline): + with open(cmdline.input, "r") as ifile: + groups = ifile.readlines() + result = { + "set_file": os.path.basename(cmdline.input), + "benchmarks": [] + } + old_cwd = os.getcwd() + for raw_group in groups: + group = raw_group.strip() + if len(group) == 0 or group[0] == "#": + continue + os.chdir(os.path.join(os.path.dirname(cmdline.input), os.path.dirname(group))) + for fname in glob.glob(os.path.basename(group)): + result["benchmarks"].append(os.path.join(os.path.dirname(group), fname)) + os.chdir(old_cwd) + result["benchmarks"] = sorted(result["benchmarks"]) + os.makedirs(os.path.dirname(cmdline.output), exist_ok=True) + with open(cmdline.output, "w") as ofile: + ofile.write(json.dumps(result, sort_keys=True, indent=4)) + + +if __name__ == "__main__": + exit(_main(_build_command_line_interface())) diff --git a/scripts/SV-COMP/statsbuild.py b/scripts/SV-COMP/statsbuild.py new file mode 100755 index 0000000..df524db --- /dev/null +++ b/scripts/SV-COMP/statsbuild.py @@ -0,0 +1,72 @@ +import os +import argparse +import json +from xml2json import convert_xml_to_json + + +def _build_command_line_interface(): + parser = argparse.ArgumentParser( + description="TODO", + ) + parser.add_argument("-V", "--version", action="store_true", + help="Prints the version string of the module.") + parser.add_argument( + "input", type=str, + help="TODO") + parser.add_argument( + "output", type=str, + help="TODO" + ) + cmdline = parser.parse_args() + + if cmdline.version: + print("v.1.0") + exit(0) + + if not os.path.isdir(cmdline.input): + print("ERROR: In option 'input': The passed input directory does not exist.") + exit(1) + + if os.path.isdir(cmdline.output): + print("ERROR: In option 'output': The passed output file is an existing directory.") + exit(1) + if os.path.splitext(cmdline.output)[1].lower() != ".json": + print("ERROR: In option 'input': The passed output file does not have '.json' extension.") + exit(1) + + return cmdline + + +def build_stats_json_for_evaluation_dir(evaluation_data_root_dir, output_json_pathname): + total_stats = dict() + for xml_dir, xml_name in [(os.path.abspath(dirpath), fname) + for dirpath, _, filenames in os.walk(evaluation_data_root_dir) + for fname in filenames + if os.path.splitext(fname)[1].lower() == ".xml"]: + json_pathname = os.path.join(xml_dir, os.path.splitext(xml_name)[0] + ".json") + convert_xml_to_json(os.path.join(xml_dir, xml_name), json_pathname) + if os.path.isfile(json_pathname): + with open(json_pathname, "r") as ifile: + stats = json.loads(ifile.read()) + for name, props in stats.items(): + if name in total_stats: + total_stats[name] += props + else: + total_stats[name] = props.copy() + with open(output_json_pathname, "w") as ofile: + ofile.write(json.dumps(total_stats, sort_keys=True, indent=4)) + return 0 + + +def _main(cmdline): + retval = 0 + try: + retval = build_stats_json_for_evaluation_dir(cmdline.input, cmdline.output) + except: + retval = 2 + finally: + return retval + + +if __name__ == "__main__": + exit(_main(_build_command_line_interface())) diff --git a/scripts/SV-COMP/statsdiff.py b/scripts/SV-COMP/statsdiff.py new file mode 100755 index 0000000..9d90270 --- /dev/null +++ b/scripts/SV-COMP/statsdiff.py @@ -0,0 +1,212 @@ +import os +import argparse +import json + + +def _build_command_line_interface(): + parser = argparse.ArgumentParser( + description="TODO", + ) + parser.add_argument("-V", "--version", action="store_true", + help="Prints the version string of the module.") + parser.add_argument( + "left", type=str, + help="TODO") + parser.add_argument( + "right", type=str, + help="TODO" + ) + parser.add_argument( + "output", type=str, + help="TODO" + ) + cmdline = parser.parse_args() + + if cmdline.version: + print("v.1.0") + exit(0) + + if os.path.isdir(cmdline.left): + print("ERROR: In option 'left': The passed file is an existing directory.") + exit(1) + if os.path.splitext(cmdline.left)[1].lower() != ".json": + print("ERROR: In option 'left': The passed file does not have '.json' extension.") + exit(1) + + if os.path.isdir(cmdline.right): + print("ERROR: In option 'right': The passed file is an existing directory.") + exit(1) + if os.path.splitext(cmdline.right)[1].lower() != ".json": + print("ERROR: In option 'right': The passed file does not have '.json' extension.") + exit(1) + + if os.path.isdir(cmdline.output): + print("ERROR: In option 'output': The passed output file is an existing directory.") + exit(1) + if os.path.splitext(cmdline.output)[1].lower() != ".json": + print("ERROR: In option 'output': The passed output file does not have '.json' extension.") + exit(1) + + return cmdline + + +def parse_category_from_properties(props): + return props.strip().split(" ") + + +def parse_correct_status_int(benchmark_name, suffix): + idx_true = os.path.basename(benchmark_name).find("_true-" + suffix) + if idx_true != -1: + return 1 + if os.path.basename(benchmark_name).find("_false-" + suffix) == -1 and suffix == "valid-memtrack": + return parse_correct_status_int(benchmark_name, "valid-memsafety") + if not(os.path.basename(benchmark_name).find("_false-" + suffix) != -1): + return None + return 0 + + +def status_to_int(status, suffix): + if status is None: + return None + if status.lower() == "out of memory" or status.lower().startswith("error"): + return 2 + if status.lower() == "true" or status.lower() == "true(" + suffix + ")": + return 1 + if not (status.lower() == "false" or status.lower() == "false(" + suffix + ")") and suffix == "valid-memtrack": + return status_to_int(status, "valid-memsafety") + if not(status.lower() == "false" or status.lower() == "false(" + suffix + ")"): + return 2 + return 0 + + +def compare_status_values(correct_value, left_value, right_value): + if left_value == right_value: + return 0 if left_value == correct_value else 3 + else: + return 1 if left_value == correct_value else 2 + + +def build_diff_of_json_stats(left_json_pathname, right_json_pathname, output_json_pathname): + with open(left_json_pathname, "r") as ifile: + left = json.loads(ifile.read()) + with open(right_json_pathname, "r") as ifile: + right = json.loads(ifile.read()) + + unique_left = dict() + unique_right = dict() + both_equal_correct = dict() + both_equal_wrong = dict() + better_left = dict() + better_right = dict() + none_left = dict() + none_right = dict() + none_both = dict() + for name in left.keys() | right.keys(): + if name not in left: + assert name in right + unique_right[name] = right[name] + elif name not in right: + unique_left[name] = left[name] + else: + diff_props = dict() + for left_props in left[name]: + key = (left_props["options"], left_props["properties"]) + assert key not in diff_props + diff_props[key] = {"left": left_props["status"], "right": None} + for right_props in right[name]: + key = (right_props["options"], right_props["properties"]) + if key in diff_props: + diff_props[key]["right"] = right_props["status"] + else: + diff_props[key] = {"left": None, "right": right_props["status"]} + + for config, statuses in diff_props.items(): + for category in parse_category_from_properties(config[1]): + correct_value = parse_correct_status_int(name, category) + if correct_value is None: + print("WARNING: cannot parse correct status from category " + str(category) + " for benchmark " + str(name)) + continue + left_value = status_to_int(statuses["left"], category) + right_value = status_to_int(statuses["right"], category) + if left_value is None and right_value is None: + output_collection = none_both + elif left_value is None: + output_collection = none_left + elif right_value is None: + output_collection = none_right + else: + comparison_result = compare_status_values(correct_value, left_value, right_value) + if comparison_result == 0: + output_collection = both_equal_correct + elif comparison_result == 1: + output_collection = better_left + elif comparison_result == 2: + output_collection = better_right + else: + output_collection = both_equal_wrong + output_collection[name] = { + "options": config[0], + "properties": config[1], + "category": category, + "left_status": "NOT-PRESENT" if statuses["left"] is None else statuses["left"], + "left_status_value": "N/A" if left_value is None else left_value, + "right_status": "NOT-PRESENT" if statuses["right"] is None else statuses["right"], + "right_status_value": "N/A" if right_value is None else right_value + } + result_diff = { + "unique_left": unique_left, + "unique_right": unique_right, + "both_equal_correct": both_equal_correct, + "both_equal_wrong": both_equal_wrong, + "better_left": better_left, + "better_right": better_right, + "none_left": none_left, + "none_right": none_right, + "none_both": none_both, + "statistics": { + "num_left": len(left), + "num_left_tasks": sum(len(values) for _, values in left.items()), + "num_right": len(right), + "num_right_tasks": sum(len(values) for _, values in right.items()), + "num_unique_left": len(unique_left), + "num_unique_right": len(unique_right), + "num_both_equal_correct": len(both_equal_correct), + "num_both_equal_wrong": len(both_equal_wrong), + "num_better_left": len(better_left), + "num_better_right": len(better_right), + "num_none_left": len(none_left), + "num_none_right": len(none_right), + "num_none_both": len(none_both), + "num_diffs": ( + len(unique_left) + + len(unique_right) + + len(both_equal_correct) + + len(both_equal_wrong) + + len(better_left) + + len(better_right) + + len(none_left) + + len(none_right) + + len(none_both) + ), + } + + } + os.makedirs(os.path.dirname(output_json_pathname), exist_ok=True) + with open(output_json_pathname, "w") as ofile: + ofile.write(json.dumps(result_diff, sort_keys=True, indent=4)) + return 0 + + +def _main(cmdline): + return build_diff_of_json_stats(cmdline.left, cmdline.right, cmdline.output) + # retval = 0 + # try: + # retval = build_diff_of_json_stats(cmdline.left, cmdline.right, cmdline.output) + # except: + # retval = 2 + # finally: + # return retval + + +if __name__ == "__main__": + exit(_main(_build_command_line_interface())) diff --git a/scripts/SV-COMP/unpack.py b/scripts/SV-COMP/unpack.py new file mode 100755 index 0000000..a5e47c4 --- /dev/null +++ b/scripts/SV-COMP/unpack.py @@ -0,0 +1,48 @@ +import argparse +import os +import glob +import bz2 + + +def _build_command_line_interface(): + parser = argparse.ArgumentParser( + description="TODO", + ) + parser.add_argument("-V", "--version", action="store_true", + help="Prints the version string of the module.") + parser.add_argument( + "input", type=str, + help="TODO") + parser.add_argument( + "--erase-packages", action='store_true', + help="TODO") + cmdline = parser.parse_args() + + if cmdline.version: + print("v.1.0") + exit(0) + + if not os.path.isdir(cmdline.input): + print("ERROR: In option 'input': The passed input directory does not exist.") + exit(1) + + return cmdline + + +def _main(cmdline): + old_cwd = os.getcwd() + os.chdir(cmdline.input) + for fname in glob.glob("*.xml.bz2"): + with open(fname, "rb") as ifile: + compressed_data = ifile.read() + data = bz2.decompress(compressed_data) + dst_fname = os.path.splitext(fname)[0] + with open(dst_fname, "wb") as ofile: + ofile.write(data) + if cmdline.erase_packages: + os.remove(fname) + os.chdir(old_cwd) + + +if __name__ == "__main__": + exit(_main(_build_command_line_interface())) diff --git a/scripts/SV-COMP/witnessing.py b/scripts/SV-COMP/witnessing.py new file mode 100644 index 0000000..7351ba3 --- /dev/null +++ b/scripts/SV-COMP/witnessing.py @@ -0,0 +1,136 @@ +import os +import argparse +import subprocess +import shutil +import json + + +def _build_command_line_interface(): + parser = argparse.ArgumentParser( + description="TODO", + ) + parser.add_argument("-V", "--version", action="store_true", + help="Prints the version string of the module.") + parser.add_argument( + "benchmarks", type=str, + help="TODO" + ) + parser.add_argument( + "output", type=str, + help="TODO" + ) + cmdline = parser.parse_args() + + if cmdline.version: + print("v.1.0") + exit(0) + + if not os.path.isfile(cmdline.benchmarks): + print("ERROR: In option 'benchmarks': The passed path does not exist: " + cmdline.benchmarks) + exit(1) + if os.path.splitext(cmdline.benchmarks)[1].lower() != ".json": + print("ERROR: In option 'benchmarks': The passed file does not have '.json' extension.") + exit(1) + cmdline.output = os.path.abspath(cmdline.output) + + return cmdline + + +_this_file = os.path.abspath(__file__) +def get_script_dir(): + return os.path.dirname(_this_file) + + +def get_benchmarks_source_root_dir(): + return os.path.abspath(os.path.join(get_script_dir(), "..", "..", "sv-benchmarks-fork-marek-trtik", "c")) + + +def get_benchmarks_destination_root_dir(): + return os.path.abspath(os.path.join(get_script_dir(), "..", "..", "sv-benchmarks", "c")) + + +def get_cbmc_root_dir(): + return os.path.abspath(os.path.join(get_script_dir(), "..")) + + +def get_cpa_root_dir(): + return os.path.abspath(os.path.join(get_script_dir(), "..", "cpachecker")) + + +def get_cbmc_timeout_seconds(): + return 30 + + +def _main(cmdline): + os.makedirs(cmdline.output, exist_ok=True) + with open(cmdline.benchmarks, "r") as ifile: + benchmark_groups = json.loads(ifile.read()) + results = dict() + for group_fname in benchmark_groups: + with open(group_fname, "r") as ifile: + group = json.loads(ifile.read()) + category = os.path.splitext(group["set_file"])[0] + category = category[:category.find("-")] + for benchmark in group["benchmarks"]: + src_pathname = os.path.abspath(os.path.join(get_benchmarks_source_root_dir(), benchmark)) + dst_pathname = os.path.abspath(os.path.join(get_benchmarks_destination_root_dir(), benchmark)) + print("Processing: " + src_pathname) + os.makedirs(os.path.dirname(dst_pathname), exist_ok=True) + shutil.copy(src_pathname, dst_pathname) + + old_cwd = os.getcwd() + + os.chdir(get_cbmc_root_dir()) + subprocess.call(["python3", "./run.py", "--evaluate", "cbmc", "--timeout", str(get_cbmc_timeout_seconds())]) + + os.chdir(get_cpa_root_dir()) + # -secureMode + p = subprocess.Popen([ + "./scripts/cpa.sh", + "-witnessValidation", + "-heap", "5000m", + "-timelimit", "90s", + "-stats", + "-setprop", "witness.checkProgramHash=false", + "-setprop", "cpa.predicate.memoryAllocationsAlwaysSucceed=true", + "-setprop", "cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc", + "-setprop", "cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc", + "-setprop", "cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc", + "-setprop", "cpa.smg.deallocationFunctions=free,kfree,kfree_const", + "-witness", os.path.abspath(os.path.join(get_cbmc_root_dir(), "witness.graphml")), + "-spec", os.path.join(get_benchmarks_source_root_dir(), category + ".prp"), + "-benchmark", dst_pathname + ], + stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + output, err = p.communicate() + output_string = output.decode("utf-8") + err_string = err.decode("utf-8") + + os.makedirs(os.path.join(cmdline.output, os.path.dirname(benchmark)), exist_ok=True) + with open(os.path.join(cmdline.output, benchmark + ".txt"), "w") as ofile: + ofile.write("[[STDERR]]:\n\n" + output_string + "\n\n\n\n\n\n\n\n\n\n\n\n[[STDERR]]:\n\n" + err_string) + + result_start_index = output_string.find("Verification result:") + if result_start_index != -1: + result_end_index = output_string.find("\n", result_start_index) + key = output_string[result_start_index:result_end_index] + else: + key = "<>" + if key in results: + results[key].append(benchmark) + else: + results[key] = [benchmark] + + shutil.rmtree(os.path.dirname(dst_pathname)) + os.chdir(old_cwd) + + results["statistics"] = {} + for key, values in results.items(): + if key != "statistics": + results["statistics"][key] = len(values) + with open(os.path.join(cmdline.output, "witnessing_results.json"), "w") as ofile: + ofile.write(json.dumps(results, sort_keys=True, indent=4)) + + +if __name__ == "__main__": + exit(_main(_build_command_line_interface())) diff --git a/scripts/SV-COMP/xml2json.py b/scripts/SV-COMP/xml2json.py new file mode 100755 index 0000000..f89697f --- /dev/null +++ b/scripts/SV-COMP/xml2json.py @@ -0,0 +1,117 @@ +import os +import argparse +import xml.etree.ElementTree +import json + + +def _build_command_line_interface(): + parser = argparse.ArgumentParser( + description="TODO", + ) + parser.add_argument("-V", "--version", action="store_true", + help="Prints the version string of the module.") + parser.add_argument( + "input", type=str, + help="TODO") + parser.add_argument( + "output", type=str, + help="TODO" + ) + cmdline = parser.parse_args() + + if cmdline.version: + print("v.1.0") + exit(0) + + if not os.path.isfile(cmdline.input): + print("ERROR: In option 'input': The passed input file does not exist.") + exit(1) + if os.path.splitext(cmdline.input)[1].lower() != ".xml": + print("ERROR: In option 'input': The passed input file does not have '.xml' extension.") + exit(1) + + if os.path.isdir(cmdline.output): + print("ERROR: In option 'output': The passed output file is an existing directory.") + exit(1) + if os.path.splitext(cmdline.output)[1].lower() != ".json": + print("ERROR: In option 'input': The passed output file does not have '.json' extension.") + exit(1) + + return cmdline + + +def convert_xml_to_json(xml_pathname, json_pathname): + retval = 0 + benchmark_classification = dict() + tree = xml.etree.ElementTree.parse(xml_pathname) + for run_elem in tree.getroot().findall("run"): + if "name" not in run_elem.attrib: + print("WARNING: Found '' element without 'name' attribute. Skipping it.") + retval = 3 + continue + name = run_elem.attrib["name"] + if not isinstance(name, str) or len(name) == 0: + print("WARNING: Found '' element with wrongly formatted 'name' attribute. Skipping it.") + retval = 3 + continue + if "properties" not in run_elem.attrib: + print("WARNING: Found '' element without 'properties' attribute. Skipping it.") + retval = 3 + continue + properties = run_elem.attrib["properties"] + if not isinstance(properties, str) or len(properties) == 0: + print("WARNING: Found '' element with wrongly formatted 'properties' attribute. Skipping it.") + retval = 3 + continue + if "options" not in run_elem.attrib: + print("WARNING: Found '' element without 'options' attribute. Skipping it.") + retval = 3 + continue + options = run_elem.attrib["options"] + if not isinstance(options, str) or len(options) == 0: + print("WARNING: Found '' element with wrongly formatted 'options' attribute. Skipping it.") + retval = 3 + continue + status = None + for child in run_elem: + if "title" in child.attrib and child.attrib["title"] == "status" and "value" in child.attrib: + status = child.attrib["value"] + break + if status is None: + print("WARNING: Found '' element without 'status' classification. Skipping it.") + retval = 3 + continue + if not isinstance(status, str): + print("WARNING: Found '' element with wrongly formatted 'status' attribute. Skipping it.") + retval = 3 + continue + if len(status) == 0: + print("WARNING: Found '' element with empty 'status' attribute (perhaps incomplete result). Skipping it.") + retval = 3 + continue + record = { + "status": status, + "properties": properties, + "options": options + } + if name in benchmark_classification: + benchmark_classification[name].append(record) + else: + benchmark_classification[name] = [record] + with open(json_pathname, "w") as ofile: + ofile.write(json.dumps(benchmark_classification, sort_keys=True, indent=4)) + return retval + + +def _main(cmdline): + retval = 0 + try: + retval = convert_xml_to_json(cmdline.input, cmdline.output) + except: + retval = 2 + finally: + return retval + + +if __name__ == "__main__": + exit(_main(_build_command_line_interface()))