Potential valid-memsafety violations in Concurrency benchmarks.
I implemented support for checking valid-memsafety
in dartagnan and it reports a few violations that contradicts the expected behaviors. There is some nasty address computation going on so I am not sure if the expected result is wrong of there is a bug in our analysis.
Consider this code coming from goblint-regression/09-regions_06-ptra_nr.i
(there are similar problems with e.g. the computation of container_of
in ldv-races
benchmarks)
pthread_create(&t1, ((void *)0), t_fun, ((void *)0));
ip = &p->datum;
sp = ((struct s *)((char *)(ip)-(unsigned long)(&((struct s *)0)->datum)));
pthread_mutex_lock(&A_mutex);
I instrumented the code with UBSAN (using -fsanitize=null
) and corresponding part of the generated LLVM looks like this
%26 = call i32 @pthread_create(i64* noundef %2, %union.pthread_attr_t* noundef null, i8* (i8*)* noundef @t_fun, i8* noundef null) #4
%27 = load %struct.s*, %struct.s** %5, align 8
%28 = icmp ne %struct.s* %27, null, !nosanitize !6
br i1 %28, label %31, label %29, !prof !7, !nosanitize !6
29: ; preds = %22
%30 = ptrtoint %struct.s* %27 to i64, !nosanitize !6
call void @__ubsan_handle_type_mismatch_v1(i8* bitcast ({ { [45 x i8]*, i32, i32 }, { i16, i16, [11 x i8] }*, i8, i8 }* @18 to i8*), i64 %30) #4, !nosanitize !6
br label %31, !nosanitize !6
31: ; preds = %29, %22
%32 = getelementptr inbounds %struct.s, %struct.s* %27, i32 0, i32 1
store i32* %32, i32** %3, align 8
%33 = load i32*, i32** %3, align 8
%34 = bitcast i32* %33 to i8*
br i1 false, label %36, label %35, !prof !7, !nosanitize !6
35: ; preds = %31
call void @__ubsan_handle_type_mismatch_v1(i8* bitcast ({ { [45 x i8]*, i32, i32 }, { i16, i16, [11 x i8] }*, i8, i8 }* @19 to i8*), i64 0) #4, !nosanitize !6
br label %36, !nosanitize !6
As you can see, the last instruction of block 31 always jumps to block 35 and UBSAN would raise an error (assuming block 31 is reachable). The fact that the compiler ends up having this "always jump" makes me suspect there is something off (probably UB) with the code but I am still not convinced.
According to this link, "offsetof (this is basically what the computation of sp
is doing) cannot be implemented in standard C++ and requires compiler support". Not sure if the same applies to C.
Besides dartagnan, infer also reports a violation. However, deagle and ebmc report true
. All other tools do not give a final answer.
On the similar situation of ldf-races
, deagle and infer both agree with dartagnan about the violation and only ebmc reports true
.