[PATCH] D83660: [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in SMTConstraintManager.h.

Mon Apr 26 01:45:11 PDT 2021

steakhal added a comment.

In D83660#2715097 <https://reviews.llvm.org/D83660#2715097>, @OikawaKirie wrote:

> In D83660#2675064 <https://reviews.llvm.org/D83660#2675064>, @mikhail.ramalho wrote:
>
>> Indeed it looks like a copy & paste error, I'm surprised no one found it earlier.
>>
>> Regarding the tests, we used to have `make check-clang-analysis-z3` (or something similar) that would run only the analyzer's tests, but using Z3 as the constraint solver. It looks like this change broke it: https://reviews.llvm.org/D62445

It might worth investigating this build 'target'.

> Should the execution requirements be changed to make it run if z3 is enabled? Or just keep it as it is now?

We should keep current behavior IMO.

> If there are no other suggestions for this patch, I'd like to see it landed ASAP. I think it is a far too long period for a fix of a copy & paste error.

I investigated if we could mock the whole Z3 shared object.
Turns out, 33 Z3 functions should be mocked if we chose to mock every used function of libZ3.
Z3_dec_ref, Z3_del_config, Z3_del_context, Z3_get_app_decl, Z3_get_ast_id, Z3_get_bv_sort_size, Z3_get_numeral_string, Z3_get_sort_kind, Z3_inc_ref, Z3_is_eq_sort, Z3_mk_bv_sort, Z3_mk_config, Z3_mk_const, Z3_mk_context_rc, Z3_mk_eq, Z3_mk_int64, Z3_mk_not, Z3_mk_simple_solver, Z3_mk_string_symbol, Z3_mk_unsigned_int64, Z3_model_dec_ref, Z3_model_get_const_interp, Z3_model_has_interp, Z3_model_inc_ref, Z3_set_error_handler, Z3_set_param_value, Z3_solver_assert, Z3_solver_check, Z3_solver_dec_ref, Z3_solver_get_model, Z3_solver_inc_ref, Z3_solver_reset, Z3_to_app

I think we should mock only the `Z3_solver_check` function as done in this current patch. I don't see any immediate 'easier' and 'robust way of testing this.
**I'm gonna land this at the end of the week if no objections are made.**

PS: Even if this lands, Z3 solver will crash all over the place :D This was the reason why I did not want to 'push' this fix so hard.

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D83660/new/

https://reviews.llvm.org/D83660