Should uext bounds check?

[deian]

We ran into an issue when passing -1 (which when casted to uint32_t is a huge number) to boolector_uext; boolector crashes with a segfault. Here is some Haskell code demonstrating the bug:

PLSysSec/haskell-boolector#5

We can produce C code to trigger this, but I image ya'll already have an easier/faster way to test this.

Thanks!

[mpreiner]

Thanks for the report! I guess the segfault is because Boolector runs out of memory. I'll have a look.
Can you generate an API trace?

BTORAPITRACE=crash.trace <your-program>

[deian]

new
return 0x1c9f1f0
set_opt 0x1c9f1f0 model-gen 2
set_opt 0x1c9f1f0 auto-cleanup 1
set_opt 0x1c9f1f0 incremental 1
bool_sort 0x1c9f1f0
return s1@0x1c9f1f0 
bitvec_sort 0x1c9f1f0 1
return s1@0x1c9f1f0 
bitvec_sort 0x1c9f1f0 2
return s2@0x1c9f1f0 
bitvec_sort 0x1c9f1f0 4
return s3@0x1c9f1f0 
bitvec_sort 0x1c9f1f0 8
return s4@0x1c9f1f0 
bitvec_sort 0x1c9f1f0 16
return s5@0x1c9f1f0 
bitvec_sort 0x1c9f1f0 32
return s6@0x1c9f1f0 
bitvec_sort 0x1c9f1f0 64
return s7@0x1c9f1f0 
bitvec_sort 0x1c9f1f0 128
return s8@0x1c9f1f0 
constd 0x1c9f1f0 35
return n-2@0x1c9f1f0 
get_width 0x1c9f1f0 n-2@0x1c9f1f0 
return 8
uext 0x1c9f1f0 n-2@0x1c9f1f0 4294967289

[mpreiner]

Thanks! Issue is fixed on master with c6de121.