search

sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

LDV tasks with undefined behaviour and/or wrong verdicts #1270

Open tautschnig opened 3 years ago

tautschnig commented 3 years ago

The following tasks either aren't memory safe or have a wrong verdict for unreach-call (see CBMC's results)))):

Most likely they will need looking at one-by-one, with perhaps some systematic problems to be fixed.

mchalupa commented 3 years ago

Here are witnesses for memsafety violation for 181 of these benchmarks that I was able to confirm with CPAchecker: https://www.fi.muni.cz/~xchalup4/sv-comp/1270_witnesses_memsafety/

kfriedberger commented 3 years ago

Surprisingly most of the provided witnesses are quite short.

CPAchecker can also be executed to directly verify those files: scripts/cpa.sh -smg -spec test/programs/benchmarks/properties/valid-memsafety.prp -64 SOURCEFILE As CPAchecker might in theory overapproximate the state space and sometimes reports false alarms, a detailed investigation for those files is required.

I took a look at ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--acpi--apei--einj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i. There seems to be an invalid pointer dereference in line 4394. The minified counterexample trace is as follows:

static struct acpi_table_einj *einj_tab = 0;
CALL main()
  int tmp___7;
  ldv_initialize(); // does nothing
  tmp___7 = einj_init_2();
CALL einj_init()
  __cil_tmp10 = (acpi_string )"EINJ";
  __cil_tmp11 = 0U;
  __cil_tmp12 = (struct acpi_table_header **)(&einj_tab);
  status = acpi_get_table(__cil_tmp10, __cil_tmp11, __cil_tmp12); // does nothing?
  __cil_tmp13 = &einj_tab;
  __cil_tmp14 = *__cil_tmp13;
  rc = einj_check_table_4(__cil_tmp14);
CALL einj_check_table(struct acpi_table_einj *einj_tab___0)
  __cil_tmp3 = (unsigned long)einj_tab___0;
  __cil_tmp4 = __cil_tmp3 + 36;
  __cil_tmp5 = *((u32 *)__cil_tmp4); // dereference of pointer

Can someone confirm this? Maybe I have overlooked something.

Should the method acpi_get_table initialize the table somehow?

tautschnig commented 3 years ago

@kfriedberger I'm not as surprised that you are finding counterexamples to be short - the issues will really just be a lack of necessary initialisation, often resulting in an invalid pointer dereference as soon as such a pointer dereference occurs.