Possible performance optimisation: replacing multiple pointer dereferences with temporary variable storing dereferenced pointer

[natasha-jeppu]

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.

[martin-cs]

This is very interesting. Thank you. A good find.

I can definitely see why you would get a reduction in clauses and variables. The run-time difference is a bit more of a surprise. Does this still happen if you use different SAT solvers and / or the SMT back-end?

[natasha-jeppu]

This is very interesting. Thank you. A good find.

I can definitely see why you would get a reduction in clauses and variables. The run-time difference is a bit more of a surprise. Does this still happen if you use different SAT solvers and / or the SMT back-end?

I have tried kissat as the SAT solver on the dimacs cnf output from CBMC.
Without the optimisation, kissat takes 176sec and with the optimisation its 23sec.

[martin-cs]

Thanks; that rules out it being a MiniSAT performance issue. If it also happens with the SMT back-end it will be very interesting.

[tautschnig]

Closing as #5964 has been merged.