{"action":"created","issue":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/297","repository_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks","labels_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/297/labels{/name}","comments_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/297/comments","events_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/297/events","html_url":"https://github.com/sosy-lab/sv-benchmarks/issues/297","id":193376509,"number":297,"title":"Mislabeled (buggy) LDV benchmarks","user":{"login":"zvonimir","id":1040926,"avatar_url":"https://avatars.githubusercontent.com/u/1040926?v=3","gravatar_id":"","url":"https://api.github.com/users/zvonimir","html_url":"https://github.com/zvonimir","followers_url":"https://api.github.com/users/zvonimir/followers","following_url":"https://api.github.com/users/zvonimir/following{/other_user}","gists_url":"https://api.github.com/users/zvonimir/gists{/gist_id}","starred_url":"https://api.github.com/users/zvonimir/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/zvonimir/subscriptions","organizations_url":"https://api.github.com/users/zvonimir/orgs","repos_url":"https://api.github.com/users/zvonimir/repos","events_url":"https://api.github.com/users/zvonimir/events{/privacy}","received_events_url":"https://api.github.com/users/zvonimir/received_events","type":"User","site_admin":false},"labels":[{"id":472360268,"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/labels/issue%20with%20benchmark","name":"issue with benchmark","color":"d93f0b","default":false}],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":18,"created_at":"2016-12-04T21:18:30Z","updated_at":"2017-01-03T07:57:14Z","closed_at":"2017-01-03T07:57:14Z","body":"Here is the list of LDV benchmarks that almost certainly access unallocated memory, which can overwrite anything, which ultimately typically leads to a bug being reported:\r\n```\r\nldv-challenges/linux-3.14__linux-usb-dev__drivers-media-usb-hdpvr-hdpvr_true-unreach-call.cil.c\r\nldv-challenges/linux-3.14__linux-alloc-spinlock__drivers-net-xen-netfront_true-unreach-call.cil.c\r\nldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--pcmcia--pcmcia.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c\r\nldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--rtl8150.ko-entry_point_true-unreach-call.cil.out.c\r\nldv-challenges/linux-3.14__complex_emg__linux-drivers-clk1__drivers-net-ethernet-ethoc_true-unreach-call.cil.c\r\nldv-challenges/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c\r\nldv-challenges/linux-3.14__complex_emg__linux-drivers-clk1__drivers-net-ethernet-smsc-smsc911x_true-unreach-call.cil.c\r\nldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--seq--snd-seq.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c\r\nldv-challenges/linux-3.14__linux-drivers-clk1__drivers-net-ethernet-smsc-smsc911x_true-unreach-call.cil.c\r\nldv-linux-3.7.3/linux-3.10-rc1-43_1a-bitvector-drivers--atm--he.ko-ldv_main0_true-unreach-call.cil.out.c\r\nldv-challenges/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-xen-netfront_true-unreach-call.cil.c\r\nldv-challenges/linux-3.14__linux-drivers-clk1__drivers-net-ethernet-cadence-macb_true-unreach-call.cil.c\r\nldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--platform--exynos4-is--s5p-fimc.ko-entry_point_true-unreach-call.cil.out.c\r\nldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c\r\nldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--media--dvb-core--dvb-core.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c\r\nldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--video--fbdev--core--fb.ko-entry_point_true-unreach-call.cil.out.c\r\nldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--net--usb--r8152.ko-entry_point_true-unreach-call.cil.out.c\r\nldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c\r\nldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6007.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c\r\nldv-challenges/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-media-common-saa7146-saa7146_vv_true-unreach-call.cil.c\r\nldv-challenges/linux-3.14__complex_emg__linux-drivers-clk1__drivers-net-ethernet-cadence-macb_true-unreach-call.cil.c\r\n```\r\n\r\nNow that we removed the simple memory model requirement, we should address all these issues somehow. How should we go about this?\r\n\r\nThe simple answer is: we should just fix the benchmarks. However, finding violating memory accesses and figuring out how to actually properly allocated them is very time consuming. Based on my experience from last year, it takes me several hours per benchmark to do that properly, if not more.\r\n\r\nAlternatively, we could change the labels of these benchmarks to `false`. Maybe to start with, it would be great if others could confirm that they are observing (or not) same issues with the above benchmarks.\r\n\r\nFinally, we could exclude these benchmarks from the competition this year until they get fixed.\r\n\r\nPlease let us know your thoughts."},"comment":{"url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/comments/270064957","html_url":"https://github.com/sosy-lab/sv-benchmarks/issues/297#issuecomment-270064957","issue_url":"https://api.github.com/repos/sosy-lab/sv-benchmarks/issues/297","id":270064957,"user":{"login":"tautschnig","id":1144736,"avatar_url":"https://avatars.githubusercontent.com/u/1144736?v=3","gravatar_id":"","url":"https://api.github.com/users/tautschnig","html_url":"https://github.com/tautschnig","followers_url":"https://api.github.com/users/tautschnig/followers","following_url":"https://api.github.com/users/tautschnig/following{/other_user}","gists_url":"https://api.github.com/users/tautschnig/gists{/gist_id}","starred_url":"https://api.github.com/users/tautschnig/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tautschnig/subscriptions","organizations_url":"https://api.github.com/users/tautschnig/orgs","repos_url":"https://api.github.com/users/tautschnig/repos","events_url":"https://api.github.com/users/tautschnig/events{/privacy}","received_events_url":"https://api.github.com/users/tautschnig/received_events","type":"User","site_admin":false},"created_at":"2017-01-03T07:57:14Z","updated_at":"2017-01-03T07:57:14Z","body":"It seems nobody objected to closing (and going for actual pull requests instead) within 24 days."}}
{"actor":{"display_login":"tautschnig"}}