Skip to content

Fix a bug where dynamic objects' dependency across function call is not recognized [depends-on: #2646] #2694

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from

Conversation

zhixing-xu
Copy link
Contributor

This pull request includes #2646.
The purpose is to fix the issue raised by the failed test case from #2646. Quoting that test case here:

 #include <assert.h>
 #include <stdlib.h>
 
 static void f(int *x) { *x = 5; }
 static void g(int *x) { assert(*x == 5); }
 
 int main(int argc, char **argv)
 {
   int *x = (int*)malloc(sizeof(int));
   f(x);
   g(x);
   return 0;
 }

CBMC fails to catch the dependency for *x across function calls. Therefore, when running cbmc --full-slice, function f() would get skipped and the assertion fails.

The cause of the bug is: when passing reaching definition between functions, the states of symbols not in symbol table would be erased. The code snippet for that can be found in rd_range_domaint::transform_function_call in reaching_definition.cpp

if((ns.lookup(identifier, sym) || !sym->is_shared()) 
    && !rd.get_is_dirty()(identifier)){  
        export_cache.erase(identifier);
        ...
}

Since *x is a dynamic object, it is not in symbol table. No reaching definition information of it would get passed through function calls.

The fix 968ba27 checks for dynamic objects and do not erase them when going into function call.

One potential problem is: since the dynamic object is given name goto_rw::dynamic-object in #2646. There might be a symbol name confusion if there's a function named goto_rw with variable name start with dynamic-object in the program.

@tautschnig tautschnig self-assigned this Nov 10, 2018
@tautschnig tautschnig changed the title Fix a bug where dynamic objects' dependency across function call is not recognized Fix a bug where dynamic objects' dependency across function call is not recognized [depends-on: #2646] Feb 25, 2019
@TGWDB
Copy link
Contributor

TGWDB commented May 3, 2023

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.

@TGWDB TGWDB closed this May 3, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants