search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
197 stars 41 forks source link

Bug: Ultimate Automizer, GemCutter default config missing an error call #664

Closed Novak756 closed 5 months ago

Novak756 commented 5 months ago

Basic Info

Description

Given the following program

extern void __VERIFIER_error(void);

extern unsigned char __VERIFIER_nondet_uchar(void);
extern unsigned int __VERIFIER_nondet_uint(void);

//Helper functions for division and casts
long scast_helper(unsigned long i, unsigned char width){
    if((i & (1ULL << (width-1))) > 0){
        return (long)(((((1ULL << (width-1)) - 1) << 1) + 1) - i) * (-1) - 1;
    }
    return i;
}
unsigned long rotate_helper(unsigned long bv, unsigned long ammount, int left, int width){
    if(ammount == 0)
        return bv;
    if(left)
        return (bv << ammount) | (bv >> (width-ammount));
    return (bv >> ammount) | (bv << (width-ammount));
}

int main(){
    unsigned char T1_10527 = __VERIFIER_nondet_uchar();
    unsigned char T1_10525 = __VERIFIER_nondet_uchar();
    unsigned char T1_10526 = __VERIFIER_nondet_uchar();
    unsigned char T1_10524 = __VERIFIER_nondet_uchar();
    unsigned char T1_1783 = __VERIFIER_nondet_uchar();
    unsigned char T1_1784 = __VERIFIER_nondet_uchar();
    unsigned int T4_10524 = __VERIFIER_nondet_uint();

    if((((T4_10524))  ==  (((((((((T1_10527)))  <<  (unsigned int) (8U))  |  (((T1_10526))))  <<  (unsigned int) (8U))  |  (((T1_10525))))  <<  (unsigned int) (8U))  |  (((T1_10524)))))  ==  (1)){
        if((((T1_10527)))  <=  (unsigned int) (rotate_helper((((unsigned int) (rotate_helper((unsigned int) (rotate_helper((unsigned int) ( ((unsigned int) ( (((T1_10526)) / ((T1_1783)))) / ((T1_10526)))),0,1,8)),7,0,8))  +  ((~ ((1U)  ^  ((unsigned int) ( ((signed char)((unsigned int) ( (((T1_10527)) / ((T1_1783))))  &  ((T1_10524))) / (signed char)((T1_10525))))  |  (((0U)  -  ((T1_10525)))  &  (unsigned int) ( ((signed char)((1U)  ^  ((T1_10525))) / (signed char)((T1_10527))))))))))),6,1,32))){
            if((signed char)(unsigned int) ( (((T1_10526)) % (unsigned int) ( ((signed char)((((T1_10525))  ^  ((T1_10527)))  -  ((1U)  +  (unsigned int) (rotate_helper(((T1_10525)),1,1,8)))) % (signed char)(unsigned int) ( (((T1_1784)) % ((T1_10527))))))))  <=  (signed char)((~ ((T1_1783))))){
                __VERIFIER_error();
            }
        }
    }
    return 0;
}

running ./Ultimate -tc ./config/AutomizerReach.xml -s ./config/svcomp-Reach-64bit-Automizer_Default.epf -i bug.c returns TRUE. The expected result would be FALSE, which is also what the Bitvector config (svcomp-Reach-64bit-Automizer_Bitvector.epf) yields. The same bug is present in GemCutter, while Kojak and Taipan yield unknown.

Also note that the program does include some undefined behaviour (e.g. possible division by zero), but I would expect the Bitvector and Default config to treat it the same way.

Heizmann commented 5 months ago

Thanks for the report. We will have a closer look at this within the next days. The division by zero might be a problem. The settings that we use at the SV-COMP are optimized for programs that do not have undefined behavior.

schuessf commented 5 months ago

Also note that the program does include some undefined behaviour (e.g. possible division by zero)

The problem seems to be indeed the division by zero. I manually added a check that are variables occuring as divisor in your program are non-zero. Then your program should be still incorrect (Automizer finds an error using the bitvector translation) and we say unknown due to overapproximation using the integer translation (which is fine).

While we have implemented some approximation for bitwise operations in the integer translation, if you have a program that mainly consists of bitwise operations, you should consider the bitvector translation first (that is always precise).

but I would expect the Bitvector and Default config to treat it the same way.

This is not the case. We rely the semantics for division of SMT-LIB. In the theory of bitvectors division by zero yields the bitvector [1...1], while in the theory of integers division by zero can yield any integer.

Novak756 commented 5 months ago

Ok, thank you very much for the quick response and clarification!