<table border="1" cellspacing="0" cellpadding="8">
<tr>
<th>Issue</th>
<td>
<a href=https://github.com/llvm/llvm-project/issues/59420>59420</a>
</td>
</tr>
<tr>
<th>Summary</th>
<td>
Coherently model and do not invalidate assumed/conjured return value of const (object's member) function
</td>
</tr>
<tr>
<th>Labels</th>
<td>
enhancement,
clang:static analyzer
</td>
</tr>
<tr>
<th>Assignees</th>
<td>
</td>
</tr>
<tr>
<th>Reporter</th>
<td>
whisperity
</td>
</tr>
</table>
<pre>
I have a family of bug reports that all stem from the same general lack of modelling the size of a `vector` properly. The following code example is not a direct reduction but the gist of the idea, but the same problem has been observed on multiple projects with the underlying code, while not being exactly the same, achieving the same domain-specific purpose…
Comments are how I, a **C++-knowledgeable but NOT(!) CSA-knowledgeable developer**, would reason about things.
```cpp
#include <cstdlib>
#include <cstring>
#include <string>
#include <vector>
static void argvify(const std::string& Source,
char* Destination[],
const std::size_t Index)
{
Destination[Index] = reinterpret_cast<char*>(
std::calloc(Source.size() + 1, sizeof(char)));
std::strncpy(Destination[Index], Source.c_str(), Source.size() + 1);
}
struct Opts
{
std::string Program;
std::vector<std::string> Args;
};
void exec(const Opts& O)
{
char** Copy = new char*[O.Args.size() + 2];
// Copy is an array that has size "$ + 2", where "$" is a conjured unknown
// value.
argvify(O.Program, Copy, 0);
// (Irrelevant, only accessed the sub-objects of the array?)
Copy[O.Args.size() + 1] = nullptr;
// (FALSE) WARNING: Out of bound memory access (access exceeds upper limit
// of memory block)
// Copy's size is "$ + 2" and here I am accessing with "$ + 1" which must
// fit at all times.
}
```
I understand that modelling specific data structures is a problem of its own because the general API has to be "taught" to CSA to create the necessary bindings, but I would like to somehow turn the issue on its head and fix this family of bugs not by *fixing the modelling of `vector`* but by *fixing the modelling of conjured consts*. This latter path seems to me (disclaimer: I'm not deeply knowledgeable about the implementation details of CSA) an easier solution that has a higher chance of blasting away false positives.
The issue is likely that `O.Args.size()` is assumed to return two separate unknown(?) values? This seems very likely, as hoisting the calculation to its own variable, i.e.,
```cpp
const std::size_t Size = O.Args.size();
char** Copy = new char*[Size + 2];
// [...]
Copy[Size + 1] = nullptr;
```
does make the warnings disappear.
`O` is `const` and is the same object in both cases, which means that `O.Args` is also `const` and is also the same object. So we have `std::size_t std::vector<std::string>::size() const`, the function I'm calling, where the implicit `this` parameter is the same in both calls.
In between the two calls, there were no calls that had the chance of invalidating unknown globals, as the only other function, `argvify()` has internal linkage, and we can clearly see it is not capable of changing where `Copy` points to, only the inner elements.
I would like to propose the reasoning that
> Query member functions (that have no parameters except the implicit `this` and are taking the `this` properly as `const`) should always be assumed to return the exact same value, even across multiple calls.
Does this reasoning break down somewhere? The only way for such a function to have a meaningful "state" outside the object is to access globals or `thread_local`s, right? Shouldn't we conservatively assume that programs are not designed to cheat the system and that queries will, in fact, behave as queries?
With this, we need not model what the query function does (perhaps it reads the size in `O(1)`, perhaps it has to calculate it every time...) but only register the fact that
* We have an object living at "address" `&O.Args`
* that has type `std::vector<std::string>`
* which has a member function `::size() const`, which satisfies the condition of being a *query*
* which returns `$` (a value that is unknown but has an *identity*)
* that is the same `$` in all invocations (at least in the context where all the `this`es are `&O.Args`)
And then, the constraint that needs to be solved is `MaximumIndex <= AccessedIndex`: `($ + 2) - 1 <= ($ + 1)`, which we should be capable of solving: `$ + 1 = $ + 1` is trivially true, I believe even in the case there is an overflow.
----
If needed, I should be able to produce the exploded graph for the actual translation unit, but I need help with what exact commands that can be achieved. :slightly_smiling_face:
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJyMWF1v67iu_TXuC9EgUdo0eehD2u5eFLh3Ovd0gHncoGUm1lSWPJKcNPPrD0jZzkfbfc5GkWTbFkUtkmuRxhjN1hHdF7cPxe3TFXap9uF-X5vYUjDpcFX66nD_AjXuCBA22Bh7AL-BsttCoNaHFCHVmACthZiogU3wDaSaIGJDsCVHAS1Y1O-8rvEVWWvcNj9i_iG-ilAspjvSyYdiMYU2-JaCPUzgj5pg4631e16ifUVAH9i0lsBEcD4BQmUC6QSBqk4n4x2UXRLrWxMTW-ffpiIs1ON4T5xrgy8tNVBjhJLIgS8jhR1V4B00nU2GN2qD_4t0irA3qZbFnavYvcEltruvjSVxqCS-Th-okz2Me_EzqGtDu_Hs7EHlGzTuOrakzcZoaLvQ-kiFWtQMU1vMH4rpUzFd589H3zTkUgQMBLXfw4vYhUKtC7V-LNRDoR6u353fW6q2hKUlOfFvr38UalmoWaFW8Pi2vnikoh1ZhjzbkfP4zlYQCKN3gKUX2IzbxsmpP8Vimv902_ZX1Nw4bbuKoJg_6pgqa8pi_uObu8G47Td3f3mzz5XxpnzGhMlo2HlTAYbtzmwOhVpq72KCmKpivi7m696sWsCb74LmwOTV8MU_XSNjAk8Uk3HI2ZUr5derLnY0_9DPBC-uoo9CrXqP7_rAXtjOT90-QTF_gkDGJQptoPRTY0yMWfaIT66WvYVxJ43Wel2oZT7ahHeWuK-gUA8w48DyNb9hXMTSqv8b8uwMKKdbRvBrD9lYv4_-GVPIG51c_bz7cZvi7uk8cqHTCV7bFC_hAbiMHfwe_DZg84XPQ1o8XoZ7_gPWYRvP9j8vLcka-iA9pox4oxbw-kXQhjCoNTz69iDRcrQfr98-vE54w0sQFAM3PzlboZ4L9ZyNmAjoAEPAQ-ZU5iWhyEKpQt30Fvg3Ew6F4UahlCzmzPurC1RB57jC3ad9dmg7OithvnksltfJAK56FKf4e3qWIEdjhVq-hECWdugSP-idPQBqTTFSlUmuK699memzZ2I5XzF_PqI62pUNv4NuNlSF66xtU_jGo-f1_7794DV_rv_128tv_1PM1_DaiQ6UvnMVNNT4MLjJK_pf9KGJqghd21IAaxqTPtn_9I8VLdsrrdfv45kuQluouz6SJl4GE9BVIMF8AWx6vzjNRW5OHp7xw_va6BqaLn52bmMS9EKcTEMjU4-lNpD1KewvWcxiYi8k6Y4KPapShQkh12gXKOZcG8TTb8BwdPcOStLYRcri2wv_-vcXyePkoZR8Tdht68RnSZ61iL90IEx5nSM-PzKixlWsOINsv_SiZM078aLoG2INTF1wWeNj7Iilm_2pCSuBdmM-WLriefOSm4fywNK5MR-DKB8P7zdnPQlXOjvx6xVj_QmDxEKtuYUxESymRAFaTDVEokbwaBiPZWWitmgaCpyqL4W6a8S3iqi1BzhX6kGJCQw3QdwMCC9DRQmNlSJ7fFtz_qMDwmgoQPS2k4dGUkGozbamwHzltLRgpUVm-S3gHg-wQRsJWh9NMjs6F_0_Rqj5YOadbE9XxWL6qXS5neN0ibFrmBM8BMoB23uI1GLgwA90pZaZGDJPxWL-nOHLkO0oHPoNpe2JUHuTnWZENFrd2QxH8mNS7jAYxo6XmAlNRun-roX5XsLfhIvnT_D5mKdk9J_FIRu61IPPdHb7MJlM-JGviXI08y03flnzlacIDb7ngttjcFxmUJmIbUsYLlu81z6IDBLjwv_lyjLx2MhmkgfjoPSpBo2RYt8XM18RuniRJENm2Oi_sizXL8xP4M3DnvI0Uiyml_H5b_qA44JeW4aN2Vveb9O5PEbkUuSeShrGQXKH4jPayGmYW2RowYANcZWf4nIExNqhjF6YKdOeBw5-jitBbvceBII9f7j-8lC2WVGPFWvcDq2pUAqgryDYWl9iNoXZDRFlz3bHo_HdYjE9yn5fqEwN0nE6ntiMe8dtHlxcxbBrdKAtYbAHrkgwaRjCNLZCT0yBNbqtyFduUBZTSVYGyBseXZIfWwWB0jkKQJnLzonmkvB5LPS9vOTJJJc-prOEnf-A_--YKhpqypNTi9j3WO4E3jFkWf3b9G1wGQGeuRK-D3RzGvp-XmXIT1KZsyvWcgS0ezzwkPkVE9aUx8WcMUJ9DBHtyAHq4GM8DqOneZQ_n7iaReCOmJSB8B0qTghWSQlFJtM-H4TjfYDY6Zrn-iHnkx9GfS5Z47abzrJo82hFrNm-S9FUOQZDzYuY9V1Un3_gQwYoEFY_rddouV75WMGw_M-f4U2gcYW6S5Jd3vHwjSw4AiXjlHO_zT1pHnuzNsp7C0FR14T9TH-QFxBjJ_N3R8EQz-3WCvs72KCWTrWkfMw4PMS6cwLqn3nUN5nDuCuhSnYWuYd93W_5tyTaCJ8wa6GWLYUa28gVwgDE48sO44QBC7Wc5aLjDU4e71ulQcukyEiEj3s6VgO1kkZEwhhoayJTjhAXp9BlNXC3An_2lIluiJk18h6C-VgprKpAMXJ4xaHFSNAnNsbeIR3ac_L9FdmemchakPuPi9qUjX_FzHltxGTixlAGVHtXGVnN_Yu8dpFXIRIUFtrLrXPBxXzKG65cbv9zxeUDmjgyKYMsvjq2YCpyySQxOzb5Iy6njH80bpw048btvMaRgTCBJYyilf0pEn2kni-lez9jF8ppfxmZ8-lpLTlPbhAxgS6gcTkjJH-HHjx6u6OqF_T_ww_TdI0M9VDMH7mJWPcTXJ70JTB5--XJ3LKCa5gNK05unaR1Bn1PAwmWdCoU7IZkSW-8Xw7Z3mAsNwkpmJ1By5IRMjm-QEnW0I4yTQ5YYpaHQP0w7XcUNtbvzxjz-vr6-kxnNoIPVdnw0VtxNQtP1Wnqmbq1vqIKtgHbWkhUplqdOrSQArrY96CdM-k4uwiD1GTbPNcJg2TW175p0FW9zrPI8tbyrpCqCXBNWOZMe_gZG8PNyM8NamLgrqr7ebWar_CK7meLu-nt6vZmeXdV3-PqTik1V_PZnJSeVTfTxd1qeofLzXxTVnfTK3OvpkrN1HQ1u5ktp7eTzbxa3G5mNNW0wvntsriZUoPGTqzdNRMftlfS89_frm7U9MpiSTbKa2OlyElPwgKeX04USmmLEtv-nRw6tId_KPD926ercM9Wr3kOK26m1sQUj_skkyzdP3oOo0v20HMu03rlhYTHzmeU00I9j7NXL6u5qvNQFpnnlpn7ZBbP9MNZPDDQVRfsfZ1SG5mHpP_emlR35UT7plDP7F7_dd2_ES7Us2ASC_UssPw7AAD__6vQaE4">