Left shift limits

[lwli11]

Is there a max value left shift works on? If I use the code below, it verifies, but if I comment out the line and check if val is <INT_MAX instead, I get an error:

left_shift.c:5:9: error: Undefined behaviour
        return val<<6;
               ~~~^~~
an exceptional condition occurs during the evaluation of an expression (§6.5#5)

#include <limits.h>
int test(int val){
        if (val>=0 && val<9999999){
//      if (val>=0 && val<INT_MAX){
        return val<<6;
        }
        return 0;
}
int main(){
        test(0);
        }

Also, the code in the trace file does not fully appear if I use 'INT_MAX' but does if I use 2147483647.

[PeterSewell]

Yes - left-shift is undefined behaviour in C in a couple of cases - see e.g. page 10 of http://www.cl.cam.ac.uk/users/pes20/cerberus/pldi16.pdf for the relevant part of the standard and how it's captured in the Cerberus semantics underlying CN.

…

On Mon, 2 Dec 2024 at 16:33, Letitia Li ***@***.***> wrote: Is there a max value left shift works on? If I use the code below, it verifies, but if I comment out the line and check if val is <INT_MAX instead, I get an error: left_shift.c:5:9: error: Undefined behaviour return val<<6; ~~~^~~ an exceptional condition occurs during the evaluation of an expression (§6.5#5) #include <limits.h> int test(int val){ if (val>=0 && val<9999999){ // if (val>=0 && val<INT_MAX){ return val<<6; } return 0; } int main(){ test(0); } Also, the code in the trace file does not fully appear if I use 'INT_MAX' but does if I use 2147483647. — Reply to this email directly, view it on GitHub <#731>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZUL4ZBQOXSP62DWQ3T2DSDW5AVCNFSM6AAAAABS32DX7SVHI2DSMVQWIX3LMV43ASLTON2WKOZSG4YTENJUGQYDAMY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[lwli11]

Thanks, but I'm not sure I understand the Core syntax in the paper. What's the max value v can be? (It wasn't 2^15 either as I guessed).

[PeterSewell]

It isn't a simple constant - the Cerberus check does what the standard text on the left says: "If E1 has a signed type and nonnegative value, and E1×(2^E2) is representable in the result type, then that is the resulting value; otherwise, the behavior is undefined."

…

On Mon, 2 Dec 2024 at 16:51, Letitia Li ***@***.***> wrote: Thanks, but I'm not sure I understand the Core syntax in the paper. What's the max value v can be? (It wasn't 2^15 either as I guessed). — Reply to this email directly, view it on GitHub <#731 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZVSIZJ2YE2F46VXX5D2DSFYJAVCNFSM6AAAAABS32DX7SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKMJSGE2DGMJVHA> . You are receiving this because you commented.Message ID: ***@***.***>

[kmemarian]

The max value of E1 for which the shift is defined depends on E2 and the promoted type of E1. In your example here, the promoted type is signed int and E2 = 6, so the max allowed value for E1 = 0x1FFFFFF (max value such that E1 * 2 ^E2 is representable in signed int).

[kmemarian]

if the promoted type of E1 was unsigned, any value of E1 would give a defined shift.

[lwli11]

Ok, that makes sense. Thanks!