Skip to content

C library: fix use of va_list for AARCH64#8366

Merged
tautschnig merged 1 commit intodiffblue:developfrom
tautschnig:fix-8357-va_list
Sep 19, 2024
Merged

C library: fix use of va_list for AARCH64#8366
tautschnig merged 1 commit intodiffblue:developfrom
tautschnig:fix-8357-va_list

Conversation

@tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Jul 2, 2024 •
edited
Loading

This is a fixup to "C model library: Support ARM64 va_list types" that

  1. only changed only a subset of the code locations that required change
    and
  2. did so with a crude workaround.

Really, we need to abide by ARM's procedure call standard for ARM64,
which mandates that va_list be a particular struct. See

https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#definition-of-va-list
and
https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#the-va-arg-macro

While at it, also add the necessary define for Visual Studio's support
of ARM64.

Fixes: #8357

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented Jul 2, 2024

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 78.36%. Comparing base (54c20cd) to head (20e7cef).

Additional details and impacted files 
@@           Coverage Diff            @@
##           develop    #8366   +/-   ##
========================================
  Coverage    78.36%   78.36%           
========================================
  Files         1726     1726           
  Lines       188382   188382           
  Branches     18240    18240           
========================================
  Hits        147629   147629           
  Misses       40753    40753

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@kroening
Copy link
Collaborator

kroening commented Jul 3, 2024

Is this something that ought to get an #ifdef ... architecture split?

@tautschnig
Copy link
Collaborator Author

tautschnig commented Jul 3, 2024

Is this something that ought to get an #ifdef ... architecture split?

Are you suggesting this for improved code clarity or for other reasons?

@kroening
Copy link
Collaborator

kroening commented Jul 4, 2024

The fact that *(void **)&args works on the other architectures seems like a coincidence to me.

@tautschnig tautschnig self-assigned this Jul 9, 2024
@lzaoral lzaoral mentioned this pull request Jul 18, 2024
Closed
@tautschnig
C library: fix use of va_list for AARCH64
40a3dbb 
This is a fixup to "C model library: Support ARM64 va_list types" that
1) only changed only a subset of the code locations that required change
   and
2) did so with a crude workaround.

Really, we need to abide by ARM's procedure call standard for ARM64,
which mandates that `va_list` be a particular struct. See

https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#definition-of-va-list
and
https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#the-va-arg-macro

While at it, also add the necessary define for Visual Studio's support
of ARM64.

Fixes: diffblue#8357
@tautschnig tautschnig changed the title fixup! C model library: Support ARM64 va_list types C library: fix use of va_list for AARCH64 Sep 18, 2024
@tautschnig
Copy link
Collaborator Author

tautschnig commented Sep 18, 2024

The fact that *(void **)&args works on the other architectures seems like a coincidence to me.

This is now fixed: we no longer use that workaround and instead have suitable code depending on arch ifdefs.

@tautschnig tautschnig removed their assignment Sep 18, 2024
@tautschnig tautschnig merged commit 9e883f5 into diffblue:develop Sep 19, 2024
@tautschnig tautschnig deleted the fix-8357-va_list branch September 19, 2024 08:12
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Sep 19, 2024
@tautschnig
Release CBMC 6.3.0
e8610a5 
This release addresses build failures on aarch64 (64-bit ARM) platforms
(via PR diffblue#8366) and for some CMake configurations (via PR diffblue#8435). Users
of loop invariants with dynamic frames have two changes to their user
experience:
1) Users will no longer need to give unwinding specifications for `do {
   ... } while(0)` loops.
2) Loop invariants that are conjunctions will be turned into more
   fine-grained properties to ease debugging of loop invariants when
   they aren't successfully proved.
@tautschnig tautschnig mentioned this pull request Sep 19, 2024
Merged
4 tasks
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Sep 19, 2024
@tautschnig
C library: Apple does not adhere to aarch64 ABI
02322ae 
The fix from diffblue#8366 must not be used on macOS as that platform still uses
`__builtin_va_list` instead of the ARM-mandated struct.
@tautschnig tautschnig mentioned this pull request Sep 19, 2024
Merged
3 tasks
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Sep 19, 2024
@tautschnig
C library: Apple does not adhere to aarch64 ABI
9c9b52e 
The fix from diffblue#8366 must not be used on macOS as that platform still uses
`__builtin_va_list` instead of the ARM-mandated struct.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Feb 9, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
a189c13 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Feb 9, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
78df872 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Feb 9, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
0eea5f0 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Feb 10, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
446726e 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Apr 29, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
142a7c8 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Jun 17, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
a152f7f 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Jun 24, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
3688f96 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Jun 24, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
ef763b0 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Jun 24, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
f8ce259 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Jun 24, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
09f177a 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Jun 25, 2025
@tautschnig
Fully support aarch64 ABI's va_list struct
0f91a44 
aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kroening kroening kroening approved these changes

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@remi-delmas-3000 remi-delmas-3000 Awaiting requested review from remi-delmas-3000 remi-delmas-3000 is a code owner

Assignees

@kroening kroening

Labels

bugfix C Front End

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

aarch64: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE

2 participants

@tautschnig @kroening