Intrinsics Audit #727
Comments
|
Added |
|
Added |
|
Created #788 for fast math intrinsics. A first attempt was made in this branch but there are some issues with this approach that require some guidance from CBMC experts. |
|
Updated to reflect status after merging #804 |
|
Marked |
|
Basically, the remaining intrinsics to be audited can be classified into 3 groups:
|
celinval
added
[F] Soundness
|
The audit has been completed and all intrinsics in the list have been reviewed. There is a small amount of remaining cleanup work to be done which is going to be tracked in the following issues: |
The intrinsics list below is based on the table recently published in #714.
The goal is for each intrinsics to:
Note: We are now focusing on fixing issues with intrinsics that we already support. New intrinsics will be added on demand.
This issue will keep track of the work done on intrinsics (a check on intrinsics will mark it as "done") and link other issues related to the implementation/rework/cleanup of intrinsics.
abort: Handled separately as non returning intrinsic.add_with_overflow: Reviewed and tested in Tests for<op>_with_overflow#1083arith_offset: Disabled in Disable unaudited intrinsics #1081assert_inhabited: Changed to emit a panic or no-op depending on type.assert_uninit_valid: Changed to emit a panic or no-op depending on type.assert_zero_valid: Changed to emit a panic or no-op depending on type.assume: Added two tests in Tests forassume#1015atomic_and: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_and_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_and_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_and_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_and_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchg: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchg_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchg_acq_failrelaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchg_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchg_acqrel_failrelaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchg_failacq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchg_failrelaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchg_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchg_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchgweak: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchgweak_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchgweak_acq_failrelaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchgweak_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchgweak_acqrel_failrelaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchgweak_failacq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchgweak_failrelaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchgweak_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_cxchgweak_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_fence: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_fence_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_fence_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_fence_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_load: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_load_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_load_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_load_unordered: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_max: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_max_acq: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_max_acqrel: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_max_rel: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_max_relaxed: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_min: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_min_acq: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_min_acqrel: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_min_rel: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_min_relaxed: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_nand: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_nand_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_nand_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_nand_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_nand_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_or: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_or_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_or_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_or_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_or_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_singlethreadfence: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_singlethreadfence_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_singlethreadfence_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_singlethreadfence_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_store: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_store_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_store_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_store_unordered: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_umax: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_umax_acq: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_umax_acqrel: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_umax_rel: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_umax_relaxed: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_umin: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_umin_acq: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_umin_acqrel: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_umin_rel: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_umin_relaxed: Unimplemented. Negative tests added in Audit: Atomic intrinsics #850atomic_xadd: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xadd_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xadd_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xadd_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xadd_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xchg: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xchg_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xchg_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xchg_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xchg_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xor: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xor_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xor_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xor_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xor_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xsub: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xsub_acq: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xsub_acqrel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xsub_rel: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25atomic_xsub_relaxed: Reviewed in Audit: Atomic intrinsics #850. Possible improvement: Extend unstable atomic tests with generic types #25bitreverse: Support added in Partial support forbitreverse#779 and testing enabled in Enable test forbitreverseintrinsic #926.blackbox: No action needed, both implementation and test look good.breakpoint: Added a test in Add a test forbreakpoint#1022bswap: Added a test in Add a test forbswap#1023caller_location: Unimplemented (see Handle newcaller_locationintrinsic the right way #374)ceilf32: Unimplemented (was disabled in Disable rounding intrinsics #1026).ceilf64: Unimplemented (was disabled in Disable rounding intrinsics #1026).copy: Disabled in Disable unaudited intrinsics #1081copy_nonoverlapping: Disabled in Disable unaudited intrinsics #1081copysignf32: Disabled in Disable unaudited intrinsics #1081copysignf64: Disabled in Disable unaudited intrinsics #1081cosf32: Added test in Add tests for trigonometric intrinsics #1043cosf64: Added test in Add tests for trigonometric intrinsics #1043ctlz: Reviewed and completed testing in Complete tests for count intrinsics #883ctlz_nonzero: Reviewed and completed testing in Complete tests for count intrinsics #883ctpop: Completed testing in Add a test forctpop#1048cttz: Reviewed and completed testing in Complete tests for count intrinsics #883cttz_nonzero: Reviewed and completed testing in Complete tests for count intrinsics #883discriminant_value: Test added in Add a test fordiscriminant_value#1021drop_in_place: Unimplemented (deprecated since 1.52 in favor ofstd::ptr::drop_in_place)exact_div: Added tests for all corner cases in More tests forexact_div#1007exp2f32: Disabled in Disable unaudited intrinsics #1081exp2f64: Disabled in Disable unaudited intrinsics #1081expf32: Disabled in Disable unaudited intrinsics #1081expf64: Disabled in Disable unaudited intrinsics #1081fabsf32: Added tests in Tests for "absolute" intrinsics #1033fabsf64: Added tests in Tests for "absolute" intrinsics #1033fadd_fast: Was implemented in Support for fast math intrinsics #804fdiv_fast: Was implemented in Support for fast math intrinsics #804. Testing can be improved (see Some fast math results cannot be practically compared #809)float_to_int_unchecked: Unimplemented.floorf32: Unimplemented (was disabled in Disable rounding intrinsics #1026).floorf64: Unimplemented (was disabled in Disable rounding intrinsics #1026).fmaf32: Disabled in Disable unaudited intrinsics #1081fmaf64: Disabled in Disable unaudited intrinsics #1081fmul_fast: Was implemented in Support for fast math intrinsics #804. Testing can be improved (see Some fast math results cannot be practically compared #809)forget: Added comment and tests in Add tests forforget#1041frem_fast: Unimplemented (see Unimplemented intrinsic:frem_fast#810)fsub_fast: Was implemented in Support for fast math intrinsics #804likely: Added a test in Add test forlikelyandunlikelyintrinsics. #851log2f32: Disabled in Disable unaudited intrinsics #1081log2f64: Disabled in Disable unaudited intrinsics #1081log10f32: Disabled in Disable unaudited intrinsics #1081log10f64: Disabled in Disable unaudited intrinsics #1081logf32: Disabled in Disable unaudited intrinsics #1081logf64: Disabled in Disable unaudited intrinsics #1081maxnumf32: Disabled in Disable unaudited intrinsics #1081maxnumf64: Disabled in Disable unaudited intrinsics #1081min_align_of: Implementation is constant-evaluated, added test in Add tests for constant-evaluated intrinsics #1042min_align_of_val: Reviewed and added tests in Basic tests forsize_of_valandmin_alig_of_val#1101 and Fix issue with value_of / align_of traits #1089minnumf32: Disabled in Disable unaudited intrinsics #1081minnumf64: Disabled in Disable unaudited intrinsics #1081move_val_init: Unimplemented.mul_with_overflow: Reviewed and tested in Tests for<op>_with_overflow#1083nearbyintf32: Unimplemented (was disabled in Disable remaining rounding intrinsics #1028).nearbyintf64: Unimplemented (was disabled in Disable remaining rounding intrinsics #1028).needs_drop: Implementation is constant-evaluated, added test in Add tests for constant-evaluated intrinsics #1042nontemporal_store: Unimplemented.offset: Reviewed in Audit foroffsetintrinsic #1094powf32: Disabled in Disable unaudited intrinsics #1081powf64: Disabled in Disable unaudited intrinsics #1081powif32: Disabled in Disable unaudited intrinsics #1081powif64: Disabled in Disable unaudited intrinsics #1081pref_align_of: Implementation is constant-evaluated, added test in Add tests for constant-evaluated intrinsics #1042prefetch_read_data: Unimplemented.prefetch_read_instruction: Unimplemented.prefetch_write_data: Unimplemented.prefetch_write_instruction: Unimplemented.ptr_guaranteed_eq: Reviewed and added tests in Audit forptr_guaranteed_<cmp>#1090ptr_guaranteed_ne: Reviewed and added tests in Audit forptr_guaranteed_<cmp>#1090ptr_offset_from: Reviewed and added tests in Audit forptr_offset_from#1099raw_eq: Reviewed and documented in Updateraw_eqdocumentation and tests #1091rintf32: Unimplemented (was disabled in Disable remaining rounding intrinsics #1028).rintf64: Unimplemented (was disabled in Disable remaining rounding intrinsics #1028).rotate_left: Improved testing in Thorough testing for rotate intrinsics #880.rotate_right: Improved testing in Thorough testing for rotate intrinsics #880.roundf32: Unimplemented (was disabled in Disable rounding intrinsics #1026).roundf64: Unimplemented (was disabled in Disable rounding intrinsics #1026).rustc_peek: Unimplemented.saturating_add: Improved testing in Move and update saturating intrinsics #853. Consider Saturating operations could use CBMC's native support #852 in the future.saturating_sub: Improved testing in Move and update saturating intrinsics #853. Consider Saturating operations could use CBMC's native support #852 in the future.sinf32: Added test in Add tests for trigonometric intrinsics #1043sinf64: Added test in Add tests for trigonometric intrinsics #1043size_of: Implementation is constant-evaluated, added test in Add tests for constant-evaluated intrinsics #1042size_of_val: Reviewed and added tests in Basic tests forsize_of_valandmin_alig_of_val#1101 and Fix issue with value_of / align_of traits #1089sqrtf32: Disabled in Disable unaudited intrinsics #1081sqrtf64: Disabled in Disable unaudited intrinsics #1081sub_with_overflow: Reviewed and tested in Tests for<op>_with_overflow#1083transmute: Handled separately as non returning intrinsic (missing case) in Handle non returning intrinsics #736. Added tests for the general case in Audit fortransmute#1104truncf32: Unimplemented (was disabled in Disable remaining rounding intrinsics #1028).truncf64: Unimplemented (was disabled in Disable remaining rounding intrinsics #1028).try: Unimplemented ("fixme" test is included) in Unimplemented:catch_unwindintrinsic #267type_id: Implementation is constant-evaluated, added test in Add tests for constant-evaluated intrinsics #1042type_name: Implementation is constant-evaluated, added test in Add tests for constant-evaluated intrinsics #1042unaligned_volatile_load: Disabled in Disable unaudited intrinsics #1081unaligned_volatile_store: Unimplemented.unchecked_add: Reviewed and added tests in Audit for unchecked intrinsics #1076unchecked_div: Reviewed and added tests in Audit for unchecked intrinsics #1076unchecked_mul: Reviewed and added tests in Audit for unchecked intrinsics #1076unchecked_rem: Reviewed and added tests in Audit for unchecked intrinsics #1076unchecked_shl: Reviewed and added tests in Audit for unchecked intrinsics #1076unchecked_shr: Reviewed and added tests in Audit for unchecked intrinsics #1076unchecked_sub: Reviewed and added tests in Audit for unchecked intrinsics #1076unlikely: Added a test in Add test forlikelyandunlikelyintrinsics. #851unreachable: Removed implementation (as it was handled byTerminatorKind::Unreachable) and added tests in Remove implementation for theunreachableintrinsic #1100variant_count: Added negative and fixme tests in Negative test case forvariant_count#854volatile_copy_memory: Disabled in Disable unaudited intrinsics #1081. Should include test for overlapping regions.volatile_copy_nonoverlapping_memory: Disabled in Disable unaudited intrinsics #1081.volatile_load: Disabled in Disable unaudited intrinsics #1081. Has to ensuresrcis properly initialized.volatile_set_memory: Unimplemented.volatile_store: Added a concurrency warning, an alignment check and two new tests.wrapping_add: Was reviewed in Fix spurious overflow counter examples. (#558) #647. Added test in Add test for wrapping intrinsics #1070.wrapping_mul: Was reviewed in Fix spurious overflow counter examples. (#558) #647. Added test in Add test for wrapping intrinsics #1070.wrapping_sub: Was reviewed in Fix spurious overflow counter examples. (#558) #647. Added test in Add test for wrapping intrinsics #1070.write_bytes: Reviewed and added tests in Audit forwrite_bytes#1102The text was updated successfully, but these errors were encountered: