analyzer Relational Substring Domain

This PR implements a relational domain tracking substring relations between string variables. It adapts Arceri et al.'s generic proposition to fit the special design of C-strings. The domain can be understood as an enhancement to the null byte array domain, taking advantage of the tracked relations to analyze strlen, strcmp, strncmp, and especially strstr with greater precision. Indeed, to ensure all functions behave as expected, we use the query system to gain necessary information on a string's allocated memory size and its length.

The PR also introduces a new analysis using the new domain, with cases for strcpy, strncpy, strcat, strncat, strlen, strstr, strcmp, and strncmp.

This PR depends on #1076 and hence should only be merged afterwards.

TODOs:

[x] Implement special in the substring analysis
[ ] Answer new queries and restructure special in base
[ ] Add regression tests

Jul 25 '23 19:07 nathanschmidt

We'll place reviews on hold until the implementation has progressed further, please ping us once that is the case @nathanschmidt !

Aug 22 '23 12:08 michael-schwarz

We have now merged #1076, so this hopefully is no longer blocked!

Dec 13 '23 10:12 michael-schwarz

We have now merged #1076, so this hopefully is no longer blocked!

Yes, thank you for finishing the other PR! I'll try my best to get around to it, but I currently have a lot of other work, so unfortunately no guarantees.

Dec 13 '23 10:12 nathanschmidt

While this is a very interesting approach, it is not yet integrated into the other analyses. Thus, we close this for now.

Jul 23 '24 11:07 jerhard