Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add support for inline ASM #2

Open
danielsn opened this issue Mar 29, 2021 · 1 comment
Open

Add support for inline ASM #2

danielsn opened this issue Mar 29, 2021 · 1 comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct
Milestone
RMC regression ru...

Comments

@danielsn
Copy link
Contributor

No description provided.

@adpaco-aws
Copy link
Contributor

We have an unsupported test available here:

rust-tests/cbmc-reg/Asm/main_fixme.rs

Adding to milestone now.

@adpaco-aws adpaco-aws added this to the RMC regression runs clean milestone Apr 16, 2021
@avanhatt avanhatt mentioned this issue Jun 9, 2021
Merged
4 tasks
adpaco-aws pushed a commit that referenced this issue Jul 15, 2021
@bors
Auto merge of #85828 - scottmcm:raw-eq, r=oli-obk
ee86f96 
Stop generating `alloca`s & `memcmp` for simple short array equality

Example:
```rust
pub fn demo(x: [u16; 6], y: [u16; 6]) -> bool { x == y }
```

Before:
```llvm
define zeroext i1 `@_ZN10playground4demo17h48537f7eac23948fE(i96` %0, i96 %1) unnamed_addr #0 {
start:
  %y = alloca [6 x i16], align 8
  %x = alloca [6 x i16], align 8
  %.0..sroa_cast = bitcast [6 x i16]* %x to i96*
  store i96 %0, i96* %.0..sroa_cast, align 8
  %.0..sroa_cast3 = bitcast [6 x i16]* %y to i96*
  store i96 %1, i96* %.0..sroa_cast3, align 8
  %_11.i.i.i = bitcast [6 x i16]* %x to i8*
  %_14.i.i.i = bitcast [6 x i16]* %y to i8*
  %bcmp.i.i.i = call i32 `@bcmp(i8*` nonnull dereferenceable(12) %_11.i.i.i, i8* nonnull dereferenceable(12) %_14.i.i.i, i64 12) #2, !alias.scope !2
  %2 = icmp eq i32 %bcmp.i.i.i, 0
  ret i1 %2
}
```
```x86
playground::demo: # `@playground::demo`
	sub	rsp, 32
	mov	qword ptr [rsp], rdi
	mov	dword ptr [rsp + 8], esi
	mov	qword ptr [rsp + 16], rdx
	mov	dword ptr [rsp + 24], ecx
	xor	rdi, rdx
	xor	esi, ecx
	or	rsi, rdi
	sete	al
	add	rsp, 32
	ret
```

After:
```llvm
define zeroext i1 `@_ZN4mini4demo17h7a8994aaa314c981E(i96` %0, i96 %1) unnamed_addr #0 {
start:
  %2 = icmp eq i96 %0, %1
  ret i1 %2
}
```
```x86
_ZN4mini4demo17h7a8994aaa314c981E:
	xor	rcx, r8
	xor	edx, r9d
	or	rdx, rcx
	sete	al
	ret
```
celinval referenced this issue in celinval/kani-dev Sep 1, 2021
@ldm0 @nikomatsakis
select obligations after check_casts
e891044 
Otherwise, we can get into a situation where you have
a subtype obligation `#1 <: #2` pending, #1 is constrained
by `check_casts`, but #2` is unaffected.

Co-authored-by: Niko Matsakis <niko@alum.mit.edu>
celinval referenced this issue in celinval/kani-dev Oct 13, 2021
@c410-f3r
Merge pull request #2 from steffahn/collect_into_array_fix_ub
13bfcb7 
Improve last commit of rust_lang#75644
@adpaco-aws adpaco-aws mentioned this issue Oct 15, 2021
Open
98 tasks
celinval referenced this issue in celinval/kani-dev Nov 16, 2021
@Lokathor
Merge pull request #2 from rust-lang/feature/initial-types
24aa1f4 
Feature/initial types
@tedinski tedinski added [E] Unsupported Construct Add support to an unsupported construct [C] Feature / Enhancement A new feature request or enhancement to an existing feature. labels Nov 9, 2022
@tedinski tedinski mentioned this issue Jan 12, 2023
Open
3 tasks
adpaco-aws added a commit to adpaco-aws/rmc that referenced this issue Mar 21, 2023
@adpaco-aws
Update representations and recommend model-checking#2
05d6f03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct
Projects
None yet
Milestone
RMC regression runs clean
Development

No branches or pull requests
4 participants
@tedinski @danielsn @celinval @adpaco-aws