1
Fork 0

Contracts core intrinsics.

These are hooks to:

  1. control whether contract checks are run
  2. allow 3rd party tools to intercept and reintepret the results of running contracts.
This commit is contained in:
Felix S. Klock II 2024-12-02 20:35:13 +00:00 committed by Celina G. Val
parent 534d79adf9
commit bcb8565f30
30 changed files with 183 additions and 6 deletions

View file

@ -132,6 +132,9 @@ pub fn intrinsic_operation_unsafety(tcx: TyCtxt<'_>, intrinsic_id: LocalDefId) -
| sym::aggregate_raw_ptr
| sym::ptr_metadata
| sym::ub_checks
| sym::contract_checks
| sym::contract_check_requires
| sym::contract_check_ensures
| sym::fadd_algebraic
| sym::fsub_algebraic
| sym::fmul_algebraic
@ -219,6 +222,18 @@ pub fn check_intrinsic_type(
}
};
(n_tps, 0, 0, inputs, output, hir::Safety::Unsafe)
} else if intrinsic_name == sym::contract_check_ensures {
// contract_check_ensures::<'a, Ret, C>(&'a Ret, C) -> bool
// where C: impl Fn(&'a Ret) -> bool,
//
// so: two type params, one lifetime param, 0 const params, two inputs, returns boolean
let p = generics.param_at(0, tcx);
let r = ty::Region::new_early_param(tcx, p.to_early_bound_region_data());
let ref_ret = Ty::new_imm_ref(tcx, r, param(1));
// let br = ty::BoundRegion { var: ty::BoundVar::ZERO, kind: ty::BrAnon };
// let ref_ret = Ty::new_imm_ref(tcx, ty::Region::new_bound(tcx, ty::INNERMOST, br), param(0));
(2, 1, 0, vec![ref_ret, param(2)], tcx.types.bool, hir::Safety::Safe)
} else {
let safety = intrinsic_operation_unsafety(tcx, intrinsic_id);
let (n_tps, n_cts, inputs, output) = match intrinsic_name {
@ -610,6 +625,11 @@ pub fn check_intrinsic_type(
sym::box_new => (1, 0, vec![param(0)], Ty::new_box(tcx, param(0))),
// contract_checks() -> bool
sym::contract_checks => (0, 0, Vec::new(), tcx.types.bool),
// contract_check_requires::<C>(C) -> bool, where C: impl Fn() -> bool
sym::contract_check_requires => (1, 0, vec![param(0)], tcx.types.bool),
sym::simd_eq
| sym::simd_ne
| sym::simd_lt