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

Add a way to assign a label for sequential memory in memory graph #52

Closed emshem closed 4 years ago

emshem commented 4 years ago

When I created a memory graph for a program that uses strcat, the memory graph looks different when the definition for strcat is linked and unlinked. strcat takes two strings (s1 and s2), adds s2 to s1 and outputs s1. As a result, in the memory graph, the output points to the same box as the input and the box is labeled "Sequence SM". I was able to get %2(s1) and %8(output) to point to the same box by creating the following stub function:

char *strcat_stub(char *restrict dest, const char *restrict src){
    void* s = sea_dsa_new();
    sea_dsa_alias(s,(void*)dest);
    return (char*) s;
}

However, the box is still labeled SM instead of Sequence SM. There should be a way to assign this label so that the stub can properly model the way strcat uses memory.

Here are the memory graphs: linked.pdf unlinked.pdf

stub.pdf Corresponding .ll file for stub.pdf: strcat_stub.zip

agurfinkel commented 4 years ago

@caballa could you add void sea_dsa_mk_seq(void *, unsigned sz) that turns a node pointed by the first argument into a sequence node with size sz

caballa commented 4 years ago

Done in commit e42029dbe9e9bc5d1fb4ca4cded780558176f3ea