Description
CBMC version: 5.12.6 (cbmc-5.12.6-47-ge06f678f2)
Operating system: macOS Catalina 10.15.6
Exact command line resulting in the issue: make result
What behaviour did you expect: Proof runtime below 10mins
What happened instead: Runtime without optimisation = ~ 5hrs, Runtime with optimisation = ~300s
To reproduce these results use the following:
Code base: awslabs/s2n
Proof: s2n_stuffer_write_reservation
Code without optimisation: https://github.com/natasha-jeppu/s2n/blob/without_opt/stuffer/s2n_stuffer.c#L38
Code with optimisation: https://github.com/natasha-jeppu/s2n/blob/with_opt/stuffer/s2n_stuffer.c#L38
Command: make result
Optimisation: Replace multiple dereferences of struct s2n_stuffer_reservation* reservation pointer with a temporary object struct s2n_stuffer_reservation reservation_obj = *reservation and use reservation_obj for subsequent struct member access. Observed runtime decrease from 5hrs to 5mins
It would be convenient if CBMC could do this for similar constructs.
This behaviour can be explained with two profiling metrics (PRs submitted):
- Solver query complexity (extension of --write-solver-stats-to) : CBMC additional profiling info: Extend solver hardness to track clauses mapped to an instruction #5480
- Points-to set metric (--show-points-to-sets) : CBMC additional profiling info: Pointer dereference, points-to set metric #5475.
Without the optimisation, the reservation pointer is dereferenced 2656 times. Here, dereferences are counted as the number of calls to value_set_dereferencet::dereference(), for a given pointer, that generates the case split expression.
The corresponding solver query complexity metric shows 10798 clauses for https://github.com/natasha-jeppu/s2n/blob/without_opt/stuffer/s2n_stuffer.c#L42 and SSA expr is evidence of the complex case split generated.
With the optimisation, the reservation pointer is dereferenced only once.
The corresponding solver query complexity metric shows a reduction in number of clauses to 3653 for https://github.com/natasha-jeppu/s2n/blob/with_opt/stuffer/s2n_stuffer.c#L49 and the SSA expr is simplified.
