esbmc icon indicating copy to clipboard operation
esbmc copied to clipboard

Published 20 hours ago • verified publisher icon esbmc

Intrinsic memset optimization

Open rafaelsamenezes opened this issue 3 years ago • 4 comments

This PR will optimize memset operations by initializing the entire object with the result of the memset. This should avoid unrolling and speed up for memset of known bounds.

Closes #635

We should review this carefully, as this is a critical part of esbmc. I will also run this on sv-benchmarks.

rafaelsamenezes avatar Feb 25 '22 11:02 rafaelsamenezes

@mikhailramalho and @lucasccordeiro Thanks for the reviews! I will actually put it back as a draft, there are 2 features still missing: symbol support and multiple dereference objects. I will address your comments, implement those features and mark it as ready again.

rafaelsamenezes avatar Feb 28 '22 17:02 rafaelsamenezes

@rafaelsamenezes: What is the status of this PR?

lucasccordeiro avatar Apr 27 '22 13:04 lucasccordeiro

@rafaelsamenezes: What is the status of this PR?

lucasccordeiro avatar May 12 '22 09:05 lucasccordeiro

@rafaelsamenezes: could you please address @fbrausse's comments?

lucasccordeiro avatar May 13 '22 12:05 lucasccordeiro

@rafaelsamenezes: as discussed, we should move forward with this PR :-)

lucasccordeiro avatar May 21 '23 21:05 lucasccordeiro

This PR:

2023-05-26T02:27:40.8875950Z Statistics:          26459 Files
2023-05-26T02:27:40.8878371Z   correct:           14378
2023-05-26T02:27:40.8900102Z     correct true:     8154
2023-05-26T02:27:40.8901427Z     correct false:    6224
2023-05-26T02:27:40.8902410Z   incorrect:            62
2023-05-26T02:27:40.8903417Z     incorrect true:     31
2023-05-26T02:27:40.8904293Z     incorrect false:    31
2023-05-26T02:27:40.8904830Z   unknown:           12019
2023-05-26T02:27:40.8905378Z   Score:             21044 (max: 43043)

Master:

Statistics:          26459 Files
  correct:           14084
    correct true:     7852
    correct false:    6232
  incorrect:            88
    incorrect true:     42
    incorrect false:    46
  unknown:           12287
  Score:             19856 (max: 43043)

From the incorrect solved:

  • 6 incorrect false (invalid-deref) became timeouts (goblint-coreutils)
  • 15 incorrect in unreach became timeouts
  • 4 incorrect true became correct false (in reachability): aws_array_list_init_dynamic_harness_negated.yml, aws_hash_iter_begin_harness_negated.yml, aws_ring_buffer_init_harness_negated.yml, and ldv-validator-v0.6/linux-stable-4ed3cba-1-100_1a-drivers--usb--serial--qcserial.ko-entry_point.cil.out.yml
  • 2 incorrect became unknown in reachability: still checking why.

Might be worth investigating those 4 incorrect true as this patch shouldn`t improve soundness.

There is two new incorrect results: loops/ludcmp.yml (was correct), and ldv-linux-3.14/linux-3.14_complex_emg_linux-kernel-locking-spinlock_drivers-net-ethernet-dlink-dl2k.cil.yml (was timeout)

rafaelsamenezes avatar May 26 '23 08:05 rafaelsamenezes

Many thanks, @rafaelsamenezes. Can I ask you to fix the code style and rebase this PR with the master?

lucasccordeiro avatar May 26 '23 08:05 lucasccordeiro

Latest PR results:

Statistics:          26459 Files
   correct:           14369
     correct true:     8148
     correct false:    6221
   incorrect:            61
     incorrect true:     30
     incorrect false:    31
   unknown:           12029
   Score:             21061 (max: 43043)

rafaelsamenezes avatar May 29 '23 12:05 rafaelsamenezes