Skip to content

Handle copy on empty str/length zero data#235

Merged
avanhatt merged 4 commits intomodel-checking:main-152-2021-06-17from
avanhatt:empty-str-memcpy
Jun 22, 2021
Merged

Handle copy on empty str/length zero data#235
avanhatt merged 4 commits intomodel-checking:main-152-2021-06-17from
avanhatt:empty-str-memcpy

Conversation

@avanhatt
Copy link
Copy Markdown
Contributor

@avanhatt avanhatt commented Jun 18, 2021

Description of changes:

Rust seems to use a special 0x1 pointer for the empty, length-zero string. C expects memcpy to take valid pointers even when the length of the copy is zero. So, to match LLVM semantics, we should only codegen a memcpy when the length is nonzero.

Resolved issues:

Resolves #234

Call-outs:

One of the test I adds fails not for the copy, but for some code to cast back to a ptr. This is a different issue.

Testing:

  • How is this change tested?
    2 new tests, one for implicit copies and one with an intrinsic. Plus a fixme.

  • Is this a refactor change?
    No

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Copy link
Copy Markdown
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM but we should keep track of the issue appearing in the intrinsic test and provide more information if possible.

Comment on lines 6 to 11
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Open an issue regarding these failures.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added, thanks!

Comment on lines 33 to 36
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this fail for both cases or just one? This information would be useful for debugging slice processing.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Both cases, added a comment to main saying that, thanks.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// THIS CHUNK causes 3 failures
// The chunk below causes 3 failures

@avanhatt avanhatt requested a review from adpaco-aws June 22, 2021 13:18
@avanhatt avanhatt merged commit cb0c5a2 into model-checking:main-152-2021-06-17 Jun 22, 2021
adpaco-aws pushed a commit that referenced this pull request Jun 23, 2021
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
adpaco-aws pushed a commit that referenced this pull request Jul 2, 2021
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
adpaco-aws pushed a commit that referenced this pull request Jul 9, 2021
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
adpaco-aws pushed a commit that referenced this pull request Jul 15, 2021
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
adpaco-aws pushed a commit that referenced this pull request Jul 26, 2021
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
adpaco-aws pushed a commit that referenced this pull request Aug 2, 2021
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
@zhassan-aws zhassan-aws mentioned this pull request Aug 6, 2021
4 tasks
adpaco-aws pushed a commit that referenced this pull request Aug 6, 2021
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
adpaco-aws pushed a commit that referenced this pull request Aug 17, 2021
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
adpaco-aws pushed a commit that referenced this pull request Aug 24, 2021
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
@avanhatt avanhatt deleted the empty-str-memcpy branch September 14, 2021 15:25
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
tedinski pushed a commit that referenced this pull request Apr 27, 2022
For consistency with LLVM semantics, only codegen an implicit memcpy when the length is nonzero.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

CBMC fails when empty string is passed by reference

2 participants