Clear caches after simplifying constraints in Z3 backend

[dnivra]

During simplification, many Z3 ASTs(and other data) are cached to speed up the process. However, these ASTs references are never freed and thus Z3 treats them as memory leaks. This PR fixes this by clearing the caches after each simplification performed by the Z3 backend.

[dnivra]

I am not sure why these test cases fail: I am unable to reproduce any of the failures in a local CI setup. I think most of these tests also failed in CI run on the branch as well. I found that Z3 raises the "invalid dec_ref" error if the reference is reference count is 0, possibly indicating that the reference was never initialized or has been destroyed already. However, from what I found, the AST is cached only in one location in Z3 backend and the reference is increased immediately after caching. Thus, I am unsure how an AST object was cached without a reference count being increased. Is the LRU cache somehow shared; perhaps two tests end up running in the same thread and that causes problems?

[ltfish]

I want to better understand the implications before merging in this PR.

[zwimer]

The new updates only clears the abstraction cache as I see; I suspect this will be harmful if we abstract similar ASTs from Z3 multiple times, or for example if we extract A, B, C, then if (A) B else C. My recommendation to solving the memory issue here is one of these:

1. Expose a toggle in the frontend to clear some / all of these. I.e. make downsize useable. Actually, we already should have this: https://github.com/angr/claripy/blob/2e85829f77df3b2823e2aad5c23a3185e27d5851/claripy/frontend.py#L210
2. Start a threading.Thread which periodically checks the memory pressure and calls downsize as needed
3. Have some other method of triggering downsize when needed.

I believe in normal use it is not frequently needed and it primarily clears cache data, so I don't know that auto-clearing it every abstraction is the way to go.

[github-actions[bot]]

This pull request has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions[bot]]

This issue has been closed due to inactivity.

[zwimer]

@ltfish Ping

[github-actions[bot]]

Unit Test Results

   104 files  +     94     104 suites  +94   1h 0m 4s :stopwatch: + 59m 38s 1 333 tests +1 032  1 248 :heavy_check_mark: +1 007  84 :zzz: +24  1 :x: +1  1 339 runs  +1 038  1 254 :heavy_check_mark: +1 013  84 :zzz: +24  1 :x: +1 

For more details on these failures, see this check.

Results for commit dda6ba0d. ± Comparison against base commit db68e64b.

This pull request removes 30 and adds 1062 tests. Note that renamed tests count towards both.

test_annotations ‑ test_duplicated_annotations_from_makelike
test_backend_smt.TestSMTLibBackend ‑ test_index_of
test_backend_smt.TestSMTLibBackend ‑ test_ne
test_backend_smt.TestSMTLibBackend ‑ test_substr_BV_mixed_index
test_backend_smt_abc.SmtLibSolverTest_ABC ‑ test_index_of_simplification
test_backend_smt_abc.SmtLibSolverTest_ABC ‑ test_or
test_backend_smt_abc.SmtLibSolverTest_ABC ‑ test_substr_BV_symbolic_index
test_backend_smt_composite.SmtLibSolverTest_Z3 ‑ test_index_of_symbolic_start_idx
test_backend_smt_composite.SmtLibSolverTest_Z3 ‑ test_prefix
test_backend_smt_composite.SmtLibSolverTest_Z3 ‑ test_substr_simplification
…

analyses.cfg_slice_to_sink.test_cfg_slice_to_sink.TestCFGSliceToSink ‑ test_add_transitions_updates_the_slice
analyses.cfg_slice_to_sink.test_cfg_slice_to_sink.TestCFGSliceToSink ‑ test_get_entrypoints_from_slice
analyses.cfg_slice_to_sink.test_cfg_slice_to_sink.TestCFGSliceToSink ‑ test_get_transitions_from_slice
analyses.cfg_slice_to_sink.test_cfg_slice_to_sink.TestCFGSliceToSink ‑ test_nodes
analyses.cfg_slice_to_sink.test_cfg_slice_to_sink.TestCFGSliceToSink ‑ test_path_between_deals_with_loops
analyses.cfg_slice_to_sink.test_cfg_slice_to_sink.TestCFGSliceToSink ‑ test_path_between_returns_True_only_if_there_exists_at_least_a_path_between_two_nodes_in_the_slice
analyses.cfg_slice_to_sink.test_cfg_slice_to_sink.TestCFGSliceToSink ‑ test_transitions_as_tuples
analyses.cfg_slice_to_sink.test_graph.TestGraph ‑ test_slice_callgraph_mutates_the_original_graph
analyses.cfg_slice_to_sink.test_graph.TestGraph ‑ test_slice_callgraph_remove_content_not_in_a_cfg_slice_to_sink
analyses.cfg_slice_to_sink.test_graph.TestGraph ‑ test_slice_cfg_graph_mutates_the_original_graph
…

This pull request removes 6 skipped tests and adds 30 skipped tests. Note that renamed tests count towards both.

test_backend_smt_composite.SmtLibSolverTest_Z3 ‑ test_index_of_symbolic_start_idx
test_backend_smt_composite.SmtLibSolverTest_Z3 ‑ test_prefix
test_backend_smt_composite.SmtLibSolverTest_Z3 ‑ test_substr_simplification
test_backend_smt_z3.SmtLibSolverTest_Z3 ‑ test_index_of_symbolic_start_idx
test_backend_smt_z3.SmtLibSolverTest_Z3 ‑ test_prefix
test_backend_smt_z3.SmtLibSolverTest_Z3 ‑ test_substr_simplification

test_cacher.TestCacher ‑ test_cacher
test_calling_convention_analysis.TestCallingConventionAnalysis ‑ test_cgc_binary1
test_calling_convention_analysis.TestCallingConventionAnalysis ‑ test_cgc_binary2
test_cfgemulated.TestCfgemulate ‑ test_cfg_0
test_cfgemulated.TestCfgemulate ‑ test_cfg_1
test_cfgemulated.TestCfgemulate ‑ test_cfg_2
test_cfgemulated.TestCfgemulate ‑ test_cfg_3
test_cfgemulated.TestCfgemulate ‑ test_cfg_4
test_cfgemulated.TestCfgemulate ‑ test_cfg_5
test_cfgemulated.TestCfgemulate ‑ test_loop_unrolling
…

:recycle: This comment has been updated with latest results.

[github-actions[bot]]

This pull request has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions[bot]]

This issue has been closed due to inactivity.