Rework of the support for builtins #1435

mikhailramalho · 2023-10-30T20:09:40Z

This PR is part of a series of PRs derived from #876: although that PR was accepted, it's been a nightmare to rebase, so I decided to split it.

This PR changes how esbmc handles builtins: we no longer need to define new names in the preprocessor (via -D), but instead check for the functions we support or abort, similar to how intrinsics are handled.

As the first implementation, this PR changes how the __sync_fetch_and_*, atomic_store/_load, and the builtin_*_overflows functions are handled. Bonus that we got rid of the 1238 defines to support all the builtin_*_overflows in the frontend.

For the polymorphic builtins (like atomic_store/load, sync_fetch_*) the implementation creates the new function bodies in the frontend. I implemented about half of them, so some are missing. I've added a __builtin_unreachable(); call to the missing implementations so esbmc will crash on unsupported calls. It should be easy to implement these new functions and it's left as an exercise to the reader.

There are also new tests for builtin_*_overflows function and atomic_load/store, which we didn't have before (these functions are used in the aws benchmarks).

fbrausse

LGTM. I have one suggestion for improvement.

src/goto-symex/builtin_functions.cpp

mikhailramalho · 2023-10-31T20:03:11Z

@fbrausse @rafaelsamenezes @lucasccordeiro folks, how do I run this on sv-comp?

It's a pretty big change, so I think we should validate this PR there, specially since it changes code related to concurrency (which I know very little about).

fbrausse · 2023-11-01T01:20:30Z

When you go to "Actions" in Github, select "Run Benchexec" and press "Run workflow" on the right, you can choose the branch to run it over. The defaults run the entire sv-benchmarks with a 30s timeout.

mikhailramalho · 2023-11-01T15:55:12Z

When you go to "Actions" in Github, select "Run Benchexec" and press "Run workflow" on the right, you can choose the branch to run it over. The defaults run the entire sv-benchmarks with a 30s timeout.

got it working but the generate diff action doesn't seem to be working. How do you folks check the results? I downloaded the output but it only contains a bunch of witnesses.

lucasccordeiro · 2023-11-01T15:57:41Z

This PR:

Statistics:          23805 Files
  correct:           14187
    correct true:     7799
    correct false:    6388
  incorrect:            21
    incorrect true:      5
    incorrect false:    16
  unknown:            959
  Score:             21570 (max: 3482)

Master:

Statistics:          23805 Files
  correct:           14205
    correct true:     7820
    correct false:    6385
  incorrect:            20
    incorrect true:      5
    incorrect false:    15
  unknown:            9580
  Score:             21625 (max: 38482)

GitHub actions: https://github.com/esbmc/esbmc/actions/runs/6710604417

mikhailramalho · 2023-11-01T16:04:02Z

Yeah, I need to know which ones failed :/

My guess is that the __builtin_unreachable() calls in the frontend are prematurely aborting verification: esbmc will crash even if the unsupported functions are never called

mikhailramalho · 2023-11-01T16:07:13Z

@rafaelsamenezes lucas told me you have a script to find out which test failed, can you share it?

rafaelsamenezes · 2023-11-01T16:47:51Z

@rafaelsamenezes lucas told me you have a script to find out which test failed, can you share it?

I just download the artifacts and run table-generator on them. So:

Download your PR artifacts from here: https://github.com/esbmc/esbmc/actions/runs/6715400579
Download the master artifacts from here: https://github.com/esbmc/esbmc/actions/runs/6710604417
Select the category that you want to compare, let's say unreach-call: table-generator $OLD-unreach-call.xml.bz2 $NEW-unreach-call.xml.bz2

fbrausse · 2023-11-01T16:54:38Z

I have these 3 helper scripts to work with the sv-comp results: sv-comp-scripts.tar.gz

unpack.sh: unpacks both, the esbmc release .zip, and the benchmark results
run-tg: runs the table generator on all (hardcoded) categories creating a new "diff-$OLD-$NEW" directory for given OLD and NEW
wrong.sh: applied to one of the *.xml.bz2 it just prints the incorrect ones to stdout

fbrausse · 2023-11-03T12:14:31Z

The Windows build fails on __sync_fetch_and_add with

D:\a\esbmc\esbmc\unit\c2goto\library\builtin_libs.test.cpp(36,5): error C3861: '__sync_fetch_and_add': identifier not found [D:\a\esbmc\esbmc\build\unit\c2goto\library\builtin_libstest.vcxproj]
D:\a\esbmc\esbmc\unit\c2goto\library\builtin_libs.test.cpp(41,5): error C3861: '__sync_fetch_and_add': identifier not found [D:\a\esbmc\esbmc\build\unit\c2goto\library\builtin_libstest.vcxproj]
D:\a\esbmc\esbmc\unit\c2goto\library\builtin_libs.test.cpp(46,5): error C3861: '__sync_fetch_and_add': identifier not found [D:\a\esbmc\esbmc\build\unit\c2goto\library\builtin_libstest.vcxproj]
D:\a\esbmc\esbmc\unit\c2goto\library\builtin_libs.test.cpp(51,5): error C3861: '__sync_fetch_and_add': identifier not found [D:\a\esbmc\esbmc\build\unit\c2goto\library\builtin_libstest.vcxproj]
D:\a\esbmc\esbmc\unit\c2goto\library\builtin_libs.test.cpp(56,5): error C3861: '__sync_fetch_and_add': identifier not found [D:\a\esbmc\esbmc\build\unit\c2goto\library\builtin_libstest.vcxproj]

mikhailramalho · 2023-12-22T17:25:21Z

This PR:

Statistics:          23805 Files
  correct:           14509
    correct true:     8066
    correct false:    6443
  incorrect:            37
    incorrect true:     14
    incorrect false:    23
  unknown:            9259
  Score:             21759 (max: 38482)

Master:

Statistics:          23805 Files
  correct:           14431
    correct true:     8004
    correct false:    6427
  incorrect:            26
    incorrect true:     15
    incorrect false:    11
  unknown:            9348
  Score:             21779 (max: 38482)

Nice improvement over master on correct results, but too many incorrect results still

mikhailramalho · 2023-12-22T18:22:29Z

I've tested all the new incorrect false and they are also reported by the master branch; this branch is just faster.

I'll rerun the master branch on sv-comp, but otherwise, this should be good to go.

lucasccordeiro

Thanks for submitting this PR, @mikhailramalho.

Can I ask you please to provide the names of the benchmarks that are giving incorrect results?

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

…, so their type shouldn't be the function type, but the return type Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

… easier to define an atomic scope there Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

…since its symbol was already added in during convert Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

lucasccordeiro · 2023-12-23T08:59:58Z

@rafaelsamenezes: Is our windows CI broken?

mikhailramalho · 2023-12-23T14:21:29Z

@rafaelsamenezes: Is our windows CI broken?

Not really, the issue is that the failing test is calling __sync_fetch_and_add, which is gcc specific.

mikhailramalho · 2023-12-23T14:25:26Z

Latest result:
This PR:

Statistics:          23805 Files
  correct:           14509
    correct true:     8066
    correct false:    6443
  incorrect:            37
    incorrect true:     14
    incorrect false:    23
  unknown:            9259
  Score:             21759 (max: 38482)

Master:

Statistics:          23805 Files
  correct:           14533
    correct true:     8089
    correct false:    6444
  incorrect:            36
    incorrect true:     14
    incorrect false:    22
  unknown:            9236
  Score:             21822 (max: 38482)

Closer results now, I'll check the missing correct true but I guess it's only noise.

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

…cc builtin Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

mikhailramalho · 2023-12-24T17:34:59Z

The CI is broken due to issue #1559, I submitted another PR to fix that first.

mikhailramalho · 2023-12-24T23:17:00Z

This should be good to go now

lucasccordeiro · 2023-12-24T23:27:04Z

Thanks for submitting this PR, @mikhailramalho.

Otherwise, `symex_function_call` would also increment pc, when a body for a builtin is not available. Bug appears to have been introduced in #1435. --------- Co-authored-by: intrigus <abc123zeus@live.de>

mikhailramalho changed the title ~~[NFC} Rework of the support for builtins~~ Rework of the support for builtins Oct 30, 2023

fbrausse approved these changes Oct 31, 2023

View reviewed changes

src/goto-symex/builtin_functions.cpp Show resolved Hide resolved

mikhailramalho requested review from lucasccordeiro and rafaelsamenezes October 31, 2023 20:01

mikhailramalho force-pushed the rework-builtins branch from 6a8a957 to 770b9cc Compare October 31, 2023 20:12

lucasccordeiro approved these changes Nov 1, 2023

View reviewed changes

mikhailramalho force-pushed the rework-builtins branch from a566e18 to 6f3ea1c Compare December 21, 2023 21:25

lucasccordeiro approved these changes Dec 23, 2023

View reviewed changes

mikhailramalho added 11 commits December 23, 2023 08:59

Improve builtin function calls

d78b92b

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Added __ESBMC_ prefix to intrinsic functions

867a265

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

No one is using __ESBMC_*abs

04e7246

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Got rid of define to change builtin_*_overflows

cd12a18

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Move __builtin_constant_p to new run_builtin

8a6e815

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Get rid of the old sync_fetch_add model

38fda76

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Moved type2name to utils

66720d0

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

New conversion function

0d946f0

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Fix type2name path

d49a149

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Fix type of atomicExpr, they are expression, not function declaration…

8eb2692

…, so their type shouldn't be the function type, but the return type Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

New file to generate polymorphic function symbols

31c03d8

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

mikhailramalho added 11 commits December 23, 2023 08:59

Handle new atomic/sync in the frontend to create the unique symbols

a685b34

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Implement atomic_load_n and atomic_store_n

8fb2680

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Moved the implementation of sync/atomics back to frontend, since it's…

8d82118

… easier to define an atomic scope there Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Test cases for atomic_load and atomic_store

d43ee2f

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Fix location function name of the new models

4a8331e

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

we need to first check if the function identifier is an poly atomic, …

527eb4e

…since its symbol was already added in during convert Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Code style

6f598e4

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Removed lambda from intrinsic_memset

5f87a09

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Don't abort when we see an unsupported builtin

9fda0a0

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Code style fixes

870e814

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

More code style

fb635b7

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

lucasccordeiro force-pushed the rework-builtins branch from 1f59cc2 to fb635b7 Compare December 23, 2023 08:59

mikhailramalho added 5 commits December 23, 2023 13:42

Unify __atomic_fetch* and __sync_fetch*

c436998

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Use standard atomic_fetch in windows, since __sync_fetch_and_* is a g…

e5cd7a3

…cc builtin Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Missing header

54b8fdd

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Forgot namespace

0cfdd05

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

Disable test on windows since this is a gcc builtin

9c75882

Signed-off-by: Mikhail R. Gadelha <mikhail@igalia.com>

mikhailramalho mentioned this pull request Dec 23, 2023

Try to run __builtin_* function without the __builtin_ prefix? #1558

Open

Merge branch 'master' into rework-builtins

cb0d2a5

lucasccordeiro merged commit 74c1cc8 into master Dec 24, 2023
10 checks passed

lucasccordeiro deleted the rework-builtins branch December 24, 2023 23:26

intrigus-lgtm mentioned this pull request Feb 3, 2025

[symex] only increment pc if builtin is actually handled #2276

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rework of the support for builtins #1435

Rework of the support for builtins #1435

mikhailramalho commented Oct 30, 2023 •

edited

Loading

fbrausse left a comment

mikhailramalho commented Oct 31, 2023

fbrausse commented Nov 1, 2023 •

edited

Loading

mikhailramalho commented Nov 1, 2023

lucasccordeiro commented Nov 1, 2023

mikhailramalho commented Nov 1, 2023

mikhailramalho commented Nov 1, 2023

rafaelsamenezes commented Nov 1, 2023

fbrausse commented Nov 1, 2023 •

edited

Loading

fbrausse commented Nov 3, 2023

mikhailramalho commented Dec 22, 2023

mikhailramalho commented Dec 22, 2023

lucasccordeiro left a comment

lucasccordeiro commented Dec 23, 2023

mikhailramalho commented Dec 23, 2023

mikhailramalho commented Dec 23, 2023

mikhailramalho commented Dec 24, 2023

mikhailramalho commented Dec 24, 2023

lucasccordeiro commented Dec 24, 2023

Rework of the support for builtins #1435

Rework of the support for builtins #1435

Conversation

mikhailramalho commented Oct 30, 2023 • edited Loading

fbrausse left a comment

Choose a reason for hiding this comment

mikhailramalho commented Oct 31, 2023

fbrausse commented Nov 1, 2023 • edited Loading

mikhailramalho commented Nov 1, 2023

lucasccordeiro commented Nov 1, 2023

mikhailramalho commented Nov 1, 2023

mikhailramalho commented Nov 1, 2023

rafaelsamenezes commented Nov 1, 2023

fbrausse commented Nov 1, 2023 • edited Loading

fbrausse commented Nov 3, 2023

mikhailramalho commented Dec 22, 2023

mikhailramalho commented Dec 22, 2023

lucasccordeiro left a comment

Choose a reason for hiding this comment

lucasccordeiro commented Dec 23, 2023

mikhailramalho commented Dec 23, 2023

mikhailramalho commented Dec 23, 2023

mikhailramalho commented Dec 24, 2023

mikhailramalho commented Dec 24, 2023

lucasccordeiro commented Dec 24, 2023

mikhailramalho commented Oct 30, 2023 •

edited

Loading

fbrausse commented Nov 1, 2023 •

edited

Loading

fbrausse commented Nov 1, 2023 •

edited

Loading