Remaining verdicts `Error (both branches dead)` on SV-COMP

[michael-schwarz]

#1587 helped fixed some of these, but unfortunately not all: Before there were 118 instances, after it, we still have 90 instances left.

Most of them are still from the hardness suite proposed in the NFM paper by Berger et al., but some are from LDV too.

• hardness-nfm22/hardness_codestructure_dependencies_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_normal_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-100_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-10_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-24.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-25_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-500_file-13.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-500_file-18.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-500_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-500_file-7.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-500_file-74.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-500_file-92.yml
• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-50_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-pe-ci_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-pe-cn_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-pe-co_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-pe-co_file-90.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-pr-ci_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-pr-ci_file-61.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-pr-cn_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-pr-cn_file-90.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-pr-co_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-ps-ci_file-24.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-ps-ci_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-ps-ci_file-98.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-ps-cn_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_filler-ps-co_file-6.yml
• hardness-nfm22/hardness_fillercode_fillercodestructure_normal_file-6.yml
• hardness-nfm22/hardness_floatingpointinfluence_has-floats_file-86.yml
• hardness-nfm22/hardness_floatingpointinfluence_no-floats_file-86.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_100-1loop_file-5.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_100-1loop_file-66.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_100-1loop_file-68.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_100-while_file-5.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_100-while_file-66.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_100-while_file-68.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_25-1loop_file-31.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_25-1loop_file-9.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_25-while_file-31.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_25-while_file-9.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_50-1loop_file-6.yml
• hardness-nfm22/hardness_loopvsstraightlinecode_50-while_file-6.yml
• hardness-nfm22/hardness_operatoramount_amount100_file-5.yml
• hardness-nfm22/hardness_operatoramount_amount100_file-66.yml
• hardness-nfm22/hardness_operatoramount_amount100_file-68.yml
• hardness-nfm22/hardness_operatoramount_amount250_file-15.yml
• hardness-nfm22/hardness_operatoramount_amount250_file-40.yml
• hardness-nfm22/hardness_operatoramount_amount250_file-41.yml
• hardness-nfm22/hardness_operatoramount_amount250_file-51.yml
• hardness-nfm22/hardness_operatoramount_amount250_file-78.yml
• hardness-nfm22/hardness_operatoramount_amount250_file-8.yml
• hardness-nfm22/hardness_operatoramount_amount250_file-9.yml
• hardness-nfm22/hardness_operatoramount_amount25_file-31.yml
• hardness-nfm22/hardness_operatoramount_amount25_file-9.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-11.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-17.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-21.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-26.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-4.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-44.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-52.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-53.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-62.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-65.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-66.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-70.yml
• hardness-nfm22/hardness_operatoramount_amount500_file-74.yml
• hardness-nfm22/hardness_operatoramount_amount50_file-6.yml
• hardness-nfm22/hardness_variablewrapping_normal_file-86.yml
• hardness-nfm22/hardness_variablewrapping_wrapper-p_file-86.yml
• hardness-nfm22/hardness_variablewrapping_wrapper-s_file-86.yml
• hardness-nfm22/hardness_variablewrapping_wrapper-sp_file-86.yml
• ldv-linux-3.4-simple/32_7_cilled_const_ok_linux-32_1-drivers--gpu--drm--vmwgfx--vmwgfx.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.yml
• ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-fs--nfs--nfsv4.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.yml
• ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--smsc--smc91c92_cs.ko-entry_point.cil.out.yml
• ldv-linux-3.14/linux-3.14_complex_emg_linux-kernel-locking-spinlock_drivers-net-ethernet-intel-e100.cil.yml
• ldv-linux-3.14/linux-3.14_complex_emg_linux-kernel-locking-spinlock_drivers-net-ethernet-smsc-smc91c92_cs.cil.yml
• ldv-linux-3.14/linux-3.14_complex_emg_linux-usb-dev_drivers-net-ethernet-natsemi-natsemi.cil.yml
• ldv-challenges/linux-3.14_complex_emg_linux-alloc-spinlock_drivers-net-ethernet-natsemi-natsemi.cil.yml
• ldv-challenges/linux-3.14_complex_emg_linux-kernel-locking-spinlock_drivers-net-ethernet-natsemi-natsemi.cil.yml

See #1697, resolved by #1699:

• hardness-nfm22/hardness_variablewrapping_normal_file-0.yml
• hardness-nfm22/hardness_floatingpointinfluence_has-floats_file-0.yml
• hardness-nfm22/hardness_floatingpointinfluence_no-floats_file-0.yml
• hardness-nfm22/hardness_variablewrapping_wrapper-a_file-0.yml
• hardness-nfm22/hardness_variablewrapping_wrapper-ap_file-0.yml
• hardness-nfm22/hardness_variablewrapping_wrapper-p_file-0.yml
• hardness-nfm22/hardness_variablewrapping_wrapper-s_file-0.yml
• hardness-nfm22/hardness_variablewrapping_wrapper-sp_file-0.yml

Resolved by not treating Mutex as Bot (#1663)

• hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-250_file-73.yml

[michael-schwarz]

An example which can be used to reproduce the problem:

//PARAM: --enable ana.int.interval  --set sem.int.signed_overflow assume_none --set ana.activated[+] abortUnless --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --sets exp.architecture 32bit
// This file is part of the SV-Benchmarks collection of verification tasks:
// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
//
// SPDX-FileCopyrightText: 2022 Jana (Philipp) Berger
//
// SPDX-License-Identifier: GPL-3.0-or-later

extern unsigned long __VERIFIER_nondet_ulong();
extern long __VERIFIER_nondet_long();
extern unsigned char __VERIFIER_nondet_uchar();
extern char __VERIFIER_nondet_char();
extern unsigned short __VERIFIER_nondet_ushort();
extern short __VERIFIER_nondet_short();
extern float __VERIFIER_nondet_float();
extern double __VERIFIER_nondet_double();
extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
void reach_error() { __assert_fail('0', 'Req1_Prop1_Batch6dependencies.c', 13, 'reach_error'); }
void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } return; }
void assume_abort_if_not(int cond) { if(!cond) { abort(); } }
unsigned char isInitial = 0;
double var_1_1 = 100.25;
double var_1_5 = 1.9;
double var_1_6 = 7.5;
double var_1_7 = 64.25;
signed long int var_1_8 = 2;
signed long int var_1_9 = 1000000000;
signed long int var_1_10 = 1000000000;
signed long int var_1_11 = 1957998270;
float var_1_12 = 50.25;
float var_1_13 = 9.8;
float var_1_14 = 25.5;
float var_1_15 = 3.5;
signed long int var_1_16 = -500;
unsigned char var_1_17 = 1;
unsigned char var_1_18 = 1;
unsigned char var_1_19 = 0;
double last_1_var_1_1 = 100.25;
signed long int last_1_var_1_8 = 2;
float last_1_var_1_12 = 50.25;
signed long int last_1_var_1_16 = -500;
unsigned char last_1_var_1_17 = 1;
unsigned char last_1_var_1_19 = 0;
void initially(void) {
}
void step(void) {
 if (last_1_var_1_17) {
  if (var_1_7 > (((((var_1_5) < 0 ) ? -(var_1_5) : (var_1_5))) * (last_1_var_1_1 * 63.375))) {
   var_1_19 = var_1_18;
  }
 } else {
  var_1_19 = var_1_18;
 }
 if ((((((- var_1_15)) > ((last_1_var_1_12 * var_1_6))) ? ((- var_1_15)) : ((last_1_var_1_12 * var_1_6)))) < var_1_5) {
  if (var_1_11 != ((((last_1_var_1_8) < (var_1_10)) ? (last_1_var_1_8) : (var_1_10)))) {
   if (last_1_var_1_19) {
    var_1_16 = last_1_var_1_8;
   }
  }
 }
 if (((((var_1_16) < (var_1_9)) ? (var_1_16) : (var_1_9))) >= (var_1_16 - var_1_11)) {
  var_1_12 = var_1_7;
 }
 var_1_8 = (((var_1_9 + var_1_10) - last_1_var_1_16) - (var_1_11 - ((((last_1_var_1_16) < 0 ) ? -(last_1_var_1_16) : (last_1_var_1_16)))));
 if (var_1_16 < var_1_11) {
  var_1_13 = ((7.3868261718112563E18f - (var_1_14 + var_1_15)) - 5.4f);
 } else {
  var_1_13 = (var_1_15 + ((((var_1_14) < (var_1_5)) ? (var_1_14) : (var_1_5))));
 }
 if (var_1_19) {
  if (var_1_8 >= var_1_8) {
   var_1_1 = (var_1_5 + var_1_6);
  } else {
   var_1_1 = (4.125 - var_1_7);
  }
 } else {
  var_1_1 = var_1_5;
 }
 var_1_17 = (((var_1_16 * var_1_9) >= ((((var_1_16) > (var_1_8)) ? (var_1_16) : (var_1_8)))) || var_1_18);
}
void updateVariables() {
 var_1_5 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_5 >= -461168.6018427382800e+13F && var_1_5 <= -1.0e-20F) || (var_1_5 <= 4611686.018427382800e+12F && var_1_5 >= 1.0e-20F ));
 var_1_6 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_6 >= -461168.6018427382800e+13F && var_1_6 <= -1.0e-20F) || (var_1_6 <= 4611686.018427382800e+12F && var_1_6 >= 1.0e-20F ));
 var_1_7 = __VERIFIER_nondet_double();
 assume_abort_if_not((var_1_7 >= 0.0F && var_1_7 <= -1.0e-20F) || (var_1_7 <= 9223372.036854765600e+12F && var_1_7 >= 1.0e-20F ));
 var_1_9 = __VERIFIER_nondet_long();
 assume_abort_if_not(var_1_9 >= 536870911);
 assume_abort_if_not(var_1_9 <= 1073741823);
 var_1_10 = __VERIFIER_nondet_long();
 assume_abort_if_not(var_1_10 >= 536870911);
 assume_abort_if_not(var_1_10 <= 1073741823);
 var_1_11 = __VERIFIER_nondet_long();
 assume_abort_if_not(var_1_11 >= 1073741823);
 assume_abort_if_not(var_1_11 <= 2147483646);
 var_1_14 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_14 >= 0.0F && var_1_14 <= -1.0e-20F) || (var_1_14 <= 2305843.009213691390e+12F && var_1_14 >= 1.0e-20F ));
 var_1_15 = __VERIFIER_nondet_float();
 assume_abort_if_not((var_1_15 >= 0.0F && var_1_15 <= -1.0e-20F) || (var_1_15 <= 2305843.009213691390e+12F && var_1_15 >= 1.0e-20F ));
 var_1_18 = __VERIFIER_nondet_uchar();
 assume_abort_if_not(var_1_18 >= 1);
 assume_abort_if_not(var_1_18 <= 1);
}
void updateLastVariables() {
 last_1_var_1_1 = var_1_1;
 last_1_var_1_8 = var_1_8;
 last_1_var_1_12 = var_1_12;
 last_1_var_1_16 = var_1_16;
 last_1_var_1_17 = var_1_17;
 last_1_var_1_19 = var_1_19;
}
int property() {
 return ((((((var_1_19 ? ((var_1_8 >= var_1_8) ? (var_1_1 == ((double) (var_1_5 + var_1_6))) : (var_1_1 == ((double) (4.125 - var_1_7)))) : (var_1_1 == ((double) var_1_5))) && (var_1_8 == ((signed long int) (((var_1_9 + var_1_10) - last_1_var_1_16) - (var_1_11 - ((((last_1_var_1_16) < 0 ) ? -(last_1_var_1_16) : (last_1_var_1_16)))))))) && ((((((var_1_16) < (var_1_9)) ? (var_1_16) : (var_1_9))) >= (var_1_16 - var_1_11)) ? (var_1_12 == ((float) var_1_7)) : 1)) && ((var_1_16 < var_1_11) ? (var_1_13 == ((float) ((7.3868261718112563E18f - (var_1_14 + var_1_15)) - 5.4f))) : (var_1_13 == ((float) (var_1_15 + ((((var_1_14) < (var_1_5)) ? (var_1_14) : (var_1_5)))))))) && (((((((- var_1_15)) > ((last_1_var_1_12 * var_1_6))) ? ((- var_1_15)) : ((last_1_var_1_12 * var_1_6)))) < var_1_5) ? ((var_1_11 != ((((last_1_var_1_8) < (var_1_10)) ? (last_1_var_1_8) : (var_1_10)))) ? (last_1_var_1_19 ? (var_1_16 == ((signed long int) last_1_var_1_8)) : 1) : 1) : 1)) && (var_1_17 == ((unsigned char) (((var_1_16 * var_1_9) >= ((((var_1_16) > (var_1_8)) ? (var_1_16) : (var_1_8)))) || var_1_18)))) && (last_1_var_1_17 ? ((var_1_7 > (((((var_1_5) < 0 ) ? -(var_1_5) : (var_1_5))) * (last_1_var_1_1 * 63.375))) ? (var_1_19 == ((unsigned char) var_1_18)) : 1) : (var_1_19 == ((unsigned char) var_1_18)))
;
}
int main(void) {
 isInitial = 1;
 initially();
 while (1) {
  updateLastVariables();
  updateVariables();
  step();
  __VERIFIER_assert(property());
  isInitial = 0;
 }
 return 0;
}

[michael-schwarz]

The first one reduces down to

//PARAM: --set sem.int.signed_overflow assume_none

int main() {
    if(500 * 1000000000 >= 0) {
        return 0;
    } else {
        return 1;
    }
}

where the problem goes away when when removes the assume_none. This looks reasonable to me though. The computation here must overflow so it would seem reasonable that we determine both branches to be dead.

[sim642]

What's the SV-COMP property for this task though? If it's not no-overflow and we find a definite signed overflow, then the task itself may already be problematic.

In general, such situations are tricky because we're trying to assign semantics where it's been left undefined — precisely what SV-COMP wants to avoid.

[michael-schwarz]

It's indeed unreach-call, but the problem is that the place where we flag must-UB may in fact not be reachable in the concrete. The other possibility is that there indeed are bugs in the test cases, Jana Berger mentioned herself that the version contributed to SV-COMP suffers from problems. (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1430)

This begs the question of what to do with the Both branches dead verdict. If we have ~90 of them we can't / don't want to fix this sort of defeats the purpose of having a separate status for them.

[michael-schwarz]

The reduced program is the same for hardness_fillercode_fillercodesize_normal_file-6.i

[sim642]

This begs the question of what to do with the Both branches dead verdict. If we have ~90 of them we can't / don't want to fix this sort of defeats the purpose of having a separate status for them.

The purpose is to avoid unsound verdicts. Of course we could just output unknown for SV-COMP, but that won't really change anything other than just hiding these instances as they were before.
It's true that these errors aren't always necessarily precise, but so far almost all cases have actually revealed problems with tasks or unsoundness in Goblint (the first exception I'm aware of is #1585).

One possible route would be to suppress them in certain cases where it's definitely sound to do so. For example:

1. If both branches contain such must signed overflow.
2. Or if both branches contain a must NULL pointer dereference.

This follows from the semantics of our error messages: the bad thing definitely happens, if it is reachable.
Technically, it's not too clear how to exactly achieve this though: information about a certain must-violation occurring in both branches needs to be provided to the dead branches check.

[michael-schwarz]

hardness-nfm22/hardness_variablewrapping_normal_file-86.yml reduces to

//PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none
int main(void) {
    unsigned short int var_1_17;

    if(var_1_17 >= 32767) {
      if(var_1_17 <= 65534) {
        if(20 * (-25 << var_1_17)) {

        }
      }
    }
  }

which is Must-UB.

[michael-schwarz]

This seems to be a very common pattern, the counter-example extracted from LDV tests is this one:

//PARAM: --set sem.int.signed_overflow assume_none --enable ana.int.interval
int main(void)
{
   int h = 31;

   if (1 << h != 0) {

   }
}

[michael-schwarz]

The issue does not surface if we check directly for 1 << h, as that yields bot directly and then goes into the fallback.