search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
847 stars 263 forks source link

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

Open natasha-jeppu opened 4 years ago

natasha-jeppu commented 4 years ago

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 Screenshot 2020-09-24 at 16 09 23

With Optimization: Point-to set size: 1 Points-to set: ['object_descriptor(symex_dynamic::dynamic_object1, 0)'] Runtime: 893.876s Screenshot 2020-09-24 at 16 09 09

feliperodri commented 3 years ago

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

hannes-steffenhagen-diffblue commented 3 years ago

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

tautschnig commented 3 years ago

@hannes-steffenhagen-diffblue and all: please make sure you are aware of https://github.com/diffblue/cbmc/pull/2193 and the discussion that triggered it.

martin-cs commented 3 years ago

https://github.com/diffblue/cbmc/pull/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 commented 2 years ago

https://github.com/diffblue/cbmc/pull/5866 fixes this issue.