Incorrect TRUE for ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--misc--legousbtower.ko_false-unreach-call.cil.c

[lucasccordeiro]

./cbmc --graphml-witness witness.graphml --64 --propertyfile ../../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--misc--legousbtower.ko_false-unreach-call.cil.c

**** WARNING: no body for function usb_deregister
aborting path on assume(false) at file ../../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--misc--legousbtower.ko_false-unreach-call.cil.c line 12299 function ldv_assert_linux_usb_urb__more_initial_at_exit thread 0
size of program expression: 27127 steps
simple slicing removed 82 assignments
Generated 251 VCC(s), 132 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with Glucose Syrup with simplifier
1531158 variables, 4497451 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 9.735s
VERIFICATION SUCCESSFUL
EC=0
TRUE

[tautschnig]

The way I have debugged these in the past is inserting lots of assert statements to figure out which is the last one that CBMC can reach.

[tautschnig]

(Well, you could actually use --cover these days, I guess.)

[lucasccordeiro]

@tautschnig: CBMC claims that this benchmark is correct for k=1 (i.e., the unwinding assertion holds). However, if I include an assert(0); in the ldv_assume_label:, then CBMC detects that and also claims that the unwinding assertion does not hold.

void ldv_assume(int expression )
{

  {
  if (expression == 0) {
    ldv_assume_label: ;
    goto ldv_assume_label;
  } else {

  }
  return;
}

I think the unwinding assertion should fail for this particular program (at least for 1k=11). However, I'm still unable to figure out the root cause of this problem.

Have you already analysed it before?

[tautschnig]

CBMC transforms label: goto label; into assume(0) (unless disabled via the option that @peterschrammel introduced to ensure soundness on the termination benchmarks). Thus the question is: is expression == 0 necessarily true at that point?

[marek-trtik]

Here are results of my investigation:

• I failed to manually prove or disprove the classification of the benchmark, because the benchmark is big and messy, and no short property-violating error trace exists (I failed to find any).

• For low unwind constant CBMC terminates with TRUE, for larger constants (e.g. 40) it timeouts (15min). Putting __VERIFIER_assert into the benchmark showed that CBMC can reach them, except those after calls to

  void ldv_stop(void) 
  { 
  
  {
  ldv_stop_label: ;
  goto ldv_stop_label;
  }
  }

• I checked other tools for error traces. Here is one of CPA-seq: linux-4.0-rc1---drivers--usb--misc--legousbtower.ko_false-unreach-call.cil.c.xml.zip I manually followed the trace through several functions, but I did not get to the end (line 12284), because the trace is long.