Propagating information from assertions that hold to subsequent lines of code using __CPROVER_assume

[natasha-jeppu]

CBMC version: 5.13.0 (cbmc-5.13.1-46-g1276c241e)
Operating system: macOS Catalina 10.15.6
Exact command line resulting in the issue: make result
What behaviour did you expect: In functions addHeader and writeRequestLine, the pRequestHeaders points to only a dynamically allocated object (points-to set size for pRequestHeaders is 1)
What happened instead: pRequestHeaders points to NULL and dynamically allocated object (points-to set size is 2)

To reproduce these results use the following:
Code base: awslabs/aws-iot-device-sdk-embedded-C
Proof: HTTPClient_InitializeRequestHeaders
Code without optimisation: https://github.com/natasha-jeppu/aws-iot-device-sdk-embedded-C/blob/njjeppu-branch/libraries/standard/http/src/http_client.c#L1118
https://github.com/natasha-jeppu/aws-iot-device-sdk-embedded-C/blob/njjeppu-branch/libraries/standard/http/src/http_client.c#L1195
Code with optimisation: https://github.com/natasha-jeppu/aws-iot-device-sdk-embedded-C/blob/assert_then_assume/libraries/standard/http/src/http_client.c#L1136
https://github.com/natasha-jeppu/aws-iot-device-sdk-embedded-C/blob/assert_then_assume/libraries/standard/http/src/http_client.c#L1216
Command: make result

Optimisation: The assertion on https://github.com/natasha-jeppu/aws-iot-device-sdk-embedded-C/blob/njjeppu-branch/libraries/standard/http/src/http_client.c#L1209 and https://github.com/natasha-jeppu/aws-iot-device-sdk-embedded-C/blob/njjeppu-branch/libraries/standard/http/src/http_client.c#L1129 always holds true. So the pRequestHeaders is not NULL in the addHeader and writeRequestLine functions. We add an equivalent assume right after to propagate this information to subsequent lines of code.

The optimisation produces about a 6% speedup (this is after applying the optimisation to a single pointer) but what's interesting here is that we can reduce the points-to set size by doing so. This also enables constant propagation thereby reducing the number of dereferences. I have attached screenshots of the points-to set reports below.

Without Optimization:
Point-to set size: 2
Points-to set: ['object_descriptor(NULL-object, 0)', 'object_descriptor(symex_dynamic::dynamic_object1, 0)']
Runtime: 957.319s

With Optimization:
Point-to set size: 1
Points-to set: ['object_descriptor(symex_dynamic::dynamic_object1, 0)']
Runtime: 893.876s

[feliperodri]

@hannes-steffenhagen-diffblue @NlightNFotis is there anyone working on this issue? Any updates? @danielsn is that low priority?

[hannes-steffenhagen-diffblue]

@feliperodri This is currently not WIP, although we'll probably be taking a look at this in the future.

[tautschnig]

@hannes-steffenhagen-diffblue and all: please make sure you are aware of #2193 and the discussion that triggered it.

[martin-cs]

#2031 - I had totally forgotten about the big discussion about the semantics of assume and assert and how they aren't dual. There is also the "are assumptions retroactive" discussion.

[feliperodri]

#5866 fixes this issue.