[Eva] Improves widenings on nested loops.
On nested loops, for each iteration of the outer loop, postpone the widening of the inner loop of [delay] iterations, [delay] being set by -eva-widening-delay. Example: while (i < n) { j = 0; while (j < 100) { j++; } i++; } On such nested loops, the fixpoint of the inner loop is independent from the outer loop. At the first iteration of the outer loop, a fixpoint is reached for the inner loop. For other iterations of the outer loop, only one iteration of the inner loop is needed to reach a new fixpoint, by only updating the variables modified by the outer loop (i here). Avoiding widening during this one iteration is crucial for precision, as the widening of the inner loop would widen the variable i, leading to an overflow alarm at i++.
Showing
- src/plugins/value/engine/basic_partitioning.ml 3 additions, 0 deletionssrc/plugins/value/engine/basic_partitioning.ml
- src/plugins/value/engine/legacy_partitioning.ml 2 additions, 0 deletionssrc/plugins/value/engine/legacy_partitioning.ml
- src/plugins/value/engine/loop_partitioning.ml 4 additions, 0 deletionssrc/plugins/value/engine/loop_partitioning.ml
- src/plugins/value/engine/partitioned_dataflow.ml 3 additions, 2 deletionssrc/plugins/value/engine/partitioned_dataflow.ml
- src/plugins/value/engine/state_partitioning.mli 1 addition, 0 deletionssrc/plugins/value/engine/state_partitioning.mli
Loading
Please register or sign in to comment