callee not simulated by caller

[igcontreras]

These examples produce a callee not simulated by caller error (each with a different number) callee-caller-errs.zip

seahorn options:
seahorn --sea-dsa-stats --horn-nondet-undef --keep-shadows=true --sea-dsa-type-aware --sea-dsa=cs -horn-inter-proc -horn-sem-lvl=mem --horn-step=large --horn-solve --horn-global-constraints=true --horn-stats --horn-singleton-aliases=true --horn-pdr-contexts=600 --horn-ignore-calloc=true --horn-ignore-memset=true --horn-shadow-mem-optimize=false --horn-iuc=1 --horn-iuc-arith=1 --horn-weak-abs=true --horn-use-mbqi=true --horn-fp-internal-writer=false <errX.bc>

[mortkever]

The same issues can be observed in the benchmarking file of MbedTLS-2.28 and gcc, Sphinx and Xalancbmk from the SPEC 2006 benchmarking suite (all error 3). This was done with the llvm 15 port and all default options.

For the mbedTLS benchmark, seaDSA correctly infers the types of the fields but assigns a different offset:

Formal param %struct.mbedtls_mpi* %1
Actual param %struct.mbedtls_mpi* %2
Callee cell=<0, Node 0x61a19fa5c200: flags=[tCSMR] size=24 types={0:i32,16:i64*,8:i64} links=[<16, unknown>->(0,0x61a19fa625f0)]  alloca sites=[]>
Caller cell=<0, Node 0x61a19fcc5590: flags=[tCSMR] size=32 types={16:i64,8:i32,24:i64*} links=[<24, unknown>->(0,0x61a19fccd550)]  alloca sites=[]>

For Sphinx the argument passed is a nullptr, and seaDSA sees this as invalid

Formal param %struct.lmclass_s** %5
Actual param %struct.lmclass_s** null
Callee cell=<0, Node 0x626e15761bb0: flags=[tCSAR] size=8 types={0:%struct.lmclass_s*} links=[<0, unknown>->(0,0x626e1575f280)]  alloca sites=[]>
Caller cell=<0, Node 0x626e15a41f90: flags=[tCSAR] size=8 types={0:%struct.lmclass_s*} links=[<0, unknown>->(0,0x626e15a413b0)]  alloca sites=[]>

Xalan: no clue, I'll look into it next week

Formal param %"class.xercesc_2_5::DTDEntityDecl"* %1
Actual param   %296 = bitcast i8* %293 to %"class.xercesc_2_5::DTDEntityDecl"*
Callee cell=<0, Node 0x5b53cf5702b0: flags=[tCSMR] size=32 types={8:i32,24:i16*} links=[<24, unknown>->(0,0x5b53cf571060)]  alloca sites=[]>
Caller cell=<32, Node 0x5b53cf59cf30: flags=[tCSMR] size=115 types={0:%"class.xercesc_2_5::XMLMsgLoader"*,64:i8*|i16*,90:i8,52:i32,97:i8,104:i8|%"class.xercesc_2_5::XMLMsgLoader"*,40:i32|i8*|i32 (...)**|i16*,28:i32,80:i8|i8*|%"class.xercesc_2_5::XMLMsgLoader"*,16:i32|i32 (...)**|%"class.xercesc_2_5::XMLMsgLoader"*,106:i8,113:i8,56:i8*|i16*,82:i8,44:i32,89:i8,96:i8|i8*|%"class.xercesc_2_5::XMLMsgLoader"*,32:i32|i8*|i32 (...)**|%"class.xercesc_2_5::XMLMsgLoader"*|i16*,20:i32,8:i32 (...)**|%"class.xercesc_2_5::XMLMsgLoader"*,72:i8*|%"class.xercesc_2_5::XMLMsgLoader"*,98:i8,105:i8,112:i8,48:i32|i8*|i16*,36:i32,81:i8,88:i8|i8*|%"class.xercesc_2_5::XMLMsgLoader"*,24:i32|i8*|i32 (...)**|%"class.xercesc_2_5::XMLMsgLoader"*,114:i8} links=[<0, unknown>->(0,0x5b53cf5b07e0),<8, unknown>->(0,0x5b53cf5b07e0),<16, unknown>->(0,0x5b53cf5b07e0),<24, unknown>->(0,0x5b53cf5b07e0),<32, unknown>->(0,0x5b53cf5b07e0),<40, unknown>->(0,0x5b53cf5b07e0),<48, unknown>->(0,0x5b53cf5bd710),<56, unknown>->(0,0x5b53cf5a6770),<64, unknown>->(0,0x5b53cf5a6e00),<72, unknown>->(0,0x5b53cf5b07e0),<80, unknown>->(0,0x5b53cf5b07e0),<88, unknown>->(0,0x5b53cf5b07e0),<96, unknown>->(0,0x5b53cf5b07e0),<104, unknown>->(0,0x5b53cf5b07e0)]  alloca sites=[]>

I don't fully understand why the assertion error for gcc triggered at all.

Formal param %struct.ht* %0
Actual param   %37 = load %struct.ht*, %struct.ht** @ident_hash, align 8
Callee cell=<0, Node 0x654c1cd4ee90: flags=[tCSMR] size=128 types={32:i8*,96:%struct.ht_identifier* (%struct.ht*)*,104:i32,8:i8*,124:i32,16:i8*,80:i8,48:i32,120:i32,88:i8*|%struct.ht_identifier**,24:i8*,108:i32} links=[<8, unknown>->(0,0x654c1cd4dd30),<16, unknown>->(0,0x654c1cd5c650),<24, unknown>->(0,0x654c1cd5c650),<32, unknown>->(0,0x654c1cd5c650),<88, unknown>->(0,0x654c1cd5afd0),<96, unknown>->(0,0x654c1cd56200)]  alloca sites=[]>
Caller cell=<0, Node 0x654c245488f0: flags=[tCSMR] size=128 types={32:i8*,96:%struct.ht_identifier* (%struct.ht*)*,104:i32,8:i8*,124:i32,16:i8*,80:i8,48:i32,120:i32,88:i8*|%struct.ht_identifier**,24:i8*,108:i32} links=[<8, unknown>->(0,0x654c2455af40),<16, unknown>->(0,0x654c24561e80),<24, unknown>->(0,0x654c24561e80),<32, unknown>->(0,0x654c24561e80),<88, unknown>->(0,0x654c2455e530),<96, unknown>->(0,0x654c24551230)]  alloca sites=[]>

Should seaDSA already handle these correctly? Or should I compile some more information? Any way I can help fix these issues?