Calls to unknown functions in SV-COMP #1239
Comments
I'm not sure what this means. Are we somehow calling heap memory? |
This is what the call looks like, the warning is issued in the last line here. static int dibusb_thomson_tuner_attach(struct dvb_usb_adapter *adap )
{
[...]
tmp___9 = (struct dvb_frontend *(*)(struct dvb_frontend *fe , int pll_addr , struct i2c_adapter *i2c , unsigned int pll_desc_id ))tmp___10;
__a = tmp___9;
__cil_tmp16 = 0 * 360UL;
__cil_tmp17 = 1600 + __cil_tmp16;
__cil_tmp18 = (unsigned long )adap;
__cil_tmp19 = __cil_tmp18 + __cil_tmp17;
__cil_tmp20 = *((struct dvb_frontend **)__cil_tmp19);
__cil_tmp21 = *((struct dvb_usb_device **)adap);
__cil_tmp22 = (unsigned long )__cil_tmp21;
__cil_tmp23 = __cil_tmp22 + 3720;
__cil_tmp24 = (struct i2c_adapter *)__cil_tmp23;
tmp___11 = (*__a)(__cil_tmp20, 97, __cil_tmp24, 5U);
}Given the message comes from this code where let unknown_desc f =
let old_accesses (kind: AccessKind.t) args = match kind with
| Write when GobConfig.get_bool "sem.unknown_function.invalidate.args" -> args
| Write -> []
| Read when GobConfig.get_bool "sem.unknown_function.read.args" -> args
| Read -> []
| Free -> []
| Call when get_bool "sem.unknown_function.call.args" -> args
| Call -> []
| Spawn when get_bool "sem.unknown_function.spawn" -> args
| Spawn -> []
in
let attrs: LibraryDesc.attr list =
if GobConfig.get_bool "sem.unknown_function.invalidate.globals" then
[InvalidateGlobals]
else
[]
in
(* TODO: remove hack when all classify are migrated *)
if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
M.msg_final Error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing";
M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname
);
LibraryDesc.of_old ~attrs old_accesses |
|
It looks like the source in the ldv tasks is the following gem (there is modelling missing again): void *__symbol_get(const char *arg0) {
return ldv_malloc(0UL);
}tmp___10 = __symbol_get("dib3000mb_attach");
tmp___9 = (struct dvb_frontend *(*)(struct dib3000_config const *config , struct i2c_adapter *i2c ,
struct dib_fe_xfer_ops *xfer_ops ))tmp___10;
__a = tmp___9;
tmp___11 = (*__a)(__cil_tmp16, __cil_tmp20, __cil_tmp21);
// Call to __aI don't think there is anything we can fix in general here. If we are "unsound" for one of these tasks, we will just have to fight for their removal. |
|
I think we found something similar last year because I made some changes here: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1384. But the change was to consider them as valid-memsafety violation. I now see that all the cases are from MemSafety runs, so this is a non-issue as long as we actually consider the dereference invalid. It should be regardless of being a function pointer because the allocated block has size 0. |
|
In preruns from Dirk I noticed more unknown functions in Juliet tasks: |
|
From Dirk's latest prerun logs, we still have a lot of missing function definitions. Some are due to LDV benchmarks being incomplete and there's nothing we should do about it (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1398). From standard functions it seems to be I will reassign this to @karoliineh. |
Thanks, we got a bit swamped with MemSafety things here, I'm grateful if Karoliine has time to do this. |
karoliineh
added a commit
that referenced
this issue
Nov 22, 2023
karoliineh
added a commit
that referenced
this issue
Nov 22, 2023
karoliineh
added a commit
that referenced
this issue
Nov 22, 2023
sim642
added a commit
to sim642/opam-repository
that referenced
this issue
Nov 24, 2023
CHANGES: Functionally equivalent to Goblint in SV-COMP 2024. * Add termination analysis for loops (goblint/analyzer#1093). * Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197). * Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246). * Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262). * Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248). * Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191). * Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269). * Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
nberth
pushed a commit
to nberth/opam-repository
that referenced
this issue
Jun 18, 2024
CHANGES: Functionally equivalent to Goblint in SV-COMP 2024. * Add termination analysis for loops (goblint/analyzer#1093). * Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197). * Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246). * Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262). * Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248). * Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191). * Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269). * Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
On top of the missing calls to
printLongLongLine(#1237) Goblint reports the following calls to functions which are missing implementations. Most of them seem to be about missingbuiltins, which we should probably attempt to fix. (list deduplicated)LDV issues
__VERIFIER_nondet_size_t(#1242)__builtin_memcp(#1242)__builtin_strlen(#1242)__fread_unlocked_*(#1242)_Exit(#1242)_assert(#1242)The text was updated successfully, but these errors were encountered: