seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

Missing nodes for pointer variables #116

Closed shaobo-he closed 3 years ago

shaobo-he commented 3 years ago

Hello sea-dsa developers,

While I was debugging a soundness issue when using sea-dsa for SMACK, I couldn't find a node that corresponds to a pointer variable. In demo.ll, %24 of function _ZN9lru_cacheC2Ev is used as the pointer argument to a store instruction,

%24 = getelementptr inbounds %"class.std::__1::__libcpp_compressed_pair_imp.4", %"class.std::__1::__libcpp_compressed_pair_imp.4"* %23, i32 0, i32 0, !dbg !11275, !verifier.code !6341
%25 = bitcast %"struct.std::__1::__hash_node"*** %24 to i8*, !dbg !11275      
%26 = bitcast i8* inttoptr (i64 8 to i8*) to i8*, !dbg !11275                 
call void @__SMACK_check_memory_safety(i8* %25, i8* %26), !dbg !11275         
store %"struct.std::__1::__hash_node"** null, %"struct.std::__1::__hash_node"*** %24, align 8, !dbg !11275, !verifier.code !6341

I would expect it to show up in the memory graph (i.e., sgx_fopen.mem.dot),

% grep "%24 = " sgx_fopen.mem.dot
    Node0x1c4baa0 [shape=plaintext, label ="  %24 = call i8* @strncpy(i8* %22, i8* %2, i64 %23) #15, !dbg !6375, !verifier.code !6339"];
    Node0x1c6e738 [shape=plaintext, label ="  %24 = getelementptr inbounds %struct._key_request_t, %struct._key_request_t* %0, i32 0, i32 9, !dbg !6379, !verifier.code !6344"];
    Node0x201e0e8 [shape=plaintext, label ="  %24 = getelementptr inbounds %\"struct.std::__1::__list_node_base\", %\"struct.std::__1::__list_node_base\"* %23, i32 0, i32 1, !dbg !6374, !verifier.code !6339"];
    Node0x1dd98f8 [shape=plaintext, label ="  %24 = getelementptr inbounds %class.protected_fs_file, %class.protected_fs_file* %0, i32 0, i32 13, !dbg !6349, !verifier.code !6341"];

I'm using the dev10 branch and the following command to generate the memory graph (I had to change lib/seadsa/DsaPrinter.cc to let it find the graph since the entrypoint is sgx_fopen instead of `main).

seadsa -sea-dsa=ci -sea-dsa-dot demo.ll

Please let me know if it's expected or I'm missing anything. Thank you.

debug.zip

agurfinkel commented 3 years ago

Are you sure that it is still %24 in the analyzed code? The code is transformed prior to alias analysis, so it is possible that the name simply has changed.

I will look deeper, but it may take me a little time before I can get into this. Would be nice if this is not a true bug, but only a renaming :)

shaobo-he commented 3 years ago

Thank you for your quick reply. I grepped the file produced using the -oll option and it still contains %24,

$ grep "%24 = getelementptr.*%23" real.ll
  %24 = getelementptr inbounds %"class.std::__1::__libcpp_compressed_pair_imp.4", %"class.std::__1::__libcpp_compressed_pair_imp.4"* %23, i32 0, i32 0, !dbg !11275, !verifier.code !6341
  %24 = getelementptr inbounds %"struct.std::__1::__list_node_base", %"struct.std::__1::__list_node_base"* %23, i32 0, i32 1, !dbg !11820, !verifier.code !6341
caballa commented 3 years ago

@Shaobo: I'll close this issue. Open it if it's not solved yet.