Open marek-trtik opened 6 years ago
Focusing on benchmark /home/marek/root/sv-benchmarks/c/ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c
with the issue identifier dp83640_init not found
.
I was able to simplify the benchmarks into this version where the issue is still present:
static int __attribute__ ((__section__(".init.text"))) __attribute__((no_instrument_function)) dp83640_init(void) { return 0; }
int init_module(void) __attribute__((alias("dp83640_init")));;
int main()
{
dp83640_init();
return 0;
}
I think the problem here is that both the __section__
and alias
are being interpreted by the C front-end, but they probably interact poorly. I'll try to debug this.
@marek-trtik Would you be able to add a quick-hack that just comments out/removes
"section" |
"__section__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_SECTION; }
from ansi-c/scanner.l
?
Thanks for the fix. I'll do that and I'll test it on several benchmarks with the same kind of issue. But first, I need to complete the issue #11, as this has a higher priority according to @peterschrammel .
My only question here is, whether the change you proposed here is really unlikely to negatively affect results on other benchmarks.
NOTE: You should have direct write access to this repo (just like all others of the team), so that you cloud push this and any other fixes directly to the repo (i.e. without making PRs).
I've tested the fix on all the falsifiaction
benchmarks listed in the JSON file above, by running CBMC in benchexec
with 30s timeout. Here are the results:
19:32:10 ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 6.63 6.81
19:32:17 ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i TIMEOUT 60.83 61.02
19:33:19 ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i TIMEOUT 61.03 61.13
19:34:21 ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 27.21 29.48
19:34:51 ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i TIMEOUT 60.95 61.06
19:35:53 ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i TIMEOUT 60.54 61.02
19:36:54 ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 3.56 3.60
19:36:58 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 ERROR (134) 40.31 40.39
19:37:39 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 ERROR (6) 26.52 26.56
19:38:05 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 TIMEOUT 61.12 61.04
19:39:07 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 TIMEOUT 60.99 61.04
19:40:09 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 ERROR (134) 40.82 40.95
19:40:51 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 TIMEOUT 60.88 61.03
19:41:53 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 TIMEOUT 60.99 61.03
19:42:54 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 ERROR (134) 49.21 49.28
19:43:44 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 TIMEOUT 61.00 61.03
19:44:45 ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c false(unreach-call) 12.07 12.15
19:44:58 ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c ERROR (134) 6.93 6.97
19:45:05 ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c TIMEOUT 60.98 61.02
19:46:07 ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c ERROR (134) 4.60 4.63
19:46:11 ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c false(unreach-call) 4.88 4.92
19:46:16 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 TIMEOUT 60.84 61.03
19:47:18 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 TIMEOUT 61.21 61.08
19:48:22 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 TIMEOUT 60.99 61.03
19:49:23 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 TIMEOUT 60.97 61.03
19:50:25 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 TIMEOUT 61.06 61.03
19:51:27 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 TIMEOUT 61.04 61.03
19:52:28 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 TIMEOUT 61.10 61.03
19:53:30 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 TIMEOUT 61.16 61.09
19:54:33 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 TIMEOUT 60.72 61.02
19:55:34 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 TIMEOUT 61.08 61.04
19:56:36 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 TIMEOUT 60.99 61.04
19:57:38 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 TIMEOUT 60.93 61.02
19:58:39 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 TIMEOUT 60.09 60.31
19:59:41 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 TIMEOUT 60.84 61.02
20:00:43 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 TIMEOUT 60.81 61.02
20:01:44 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 TIMEOUT 60.92 61.03
20:02:46 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 TIMEOUT 60.98 61.03
20:03:48 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 TIMEOUT 61.03 61.11
20:04:51 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 TIMEOUT 61.05 61.03
20:05:53 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 TIMEOUT 60.92 61.03
20:06:55 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 TIMEOUT 60.89 61.03
20:07:56 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 TIMEOUT 61.07 61.03
20:08:58 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 TIMEOUT 60.16 60.18
20:10:00 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 TIMEOUT 60.84 61.02
20:11:01 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 TIMEOUT 60.97 61.03
20:12:03 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 TIMEOUT 60.87 61.03
20:13:05 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 TIMEOUT 60.99 61.03
20:14:06 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 TIMEOUT 60.97 61.02
20:15:08 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 TIMEOUT 60.90 61.02
20:16:10 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 TIMEOUT 60.91 61.02
So, the fix helped and it is available here: https://github.com/marek-trtik/cbmc/commit/75b3b25754c5b3607f393e58c445175e9b6c5d69 Please look at it. If confirmed correctness, I'll merge it into the main branch.
It's a cruel hack, but indeed it should just make things work for the moment. I am not actually sure it yields the right semantics, but that's probably less of a concern for the moment. We will eventually need a proper fix.
This issue is based on a search in log files from the evaluation of CBMC performed on sosy-lab computers on 24.11.2017 for the string
numeric exception
. Here is the result:Because related issue was fixed since then, results have changed for some of the benchmarks into error
identifier XYZ not found
.