radiance · commit

compiler: Check ownership transitions with immutable binding metadata

cfe03900b1cfa109486a9dfa6643e1d34a99d58bf67a75e10f57aeceedcca4ac

Alexis Sellier committed 7 days ago 1 parent 9c9a3c12

lib/std/lang/resolver.rad +33 -28

    Place,
    /// Evaluate a place prefix after checking the complete place.
    Locate,
}

/// Symbol identity and storage retained for ownership diagnostics.
/// Consumption rule for a tracked move-only binding.
union BindingUse: Copy {
    /// The binding can be consumed at most once.
    Affine,
    /// The binding must be consumed exactly once.
    Linear,
}

/// Resolved binding metadata retained for ownership checks and diagnostics.
record TrackedSymbol: Copy {
    /// Resolver-local symbol identity.
    id: u32,
    /// Symbol storage used to report ownership errors.
    symbol: *unsafe mut Symbol,
    /// Source name used in ownership diagnostics.
    name: *[u8],
    /// Declaration used to locate an unconsumed binding.
    node: *ast::Node,
    /// Consumption rule fixed before ownership analysis.
    usage: BindingUse,
}

/// Per-control-flow-path ownership state.
/// Read only the initialized symbol prefix below `len`.
record LinearEnv: Copy {
    /// Active full-region loans, indexed by the checker's regional loan table.
    regionalLoans: u64,
    /// Symbol identities and pointers. Entries below `len` are initialized.
    /// Resolved binding metadata. Entries below `len` are initialized.
    symbols: [TrackedSymbol; MAX_LINEAR_BINDINGS],
    /// Bit set for each binding that remains available.
    available: u64,
    /// Number of initialized entries in `symbols`.
    len: u32,

        return;
    }
    if env.len >= MAX_LINEAR_BINDINGS {
        throw emitError(checker.resolver, node, ErrorKind::Internal);
    }
    set env.symbols[env.len] = TrackedSymbol { id: sym.id, symbol: sym };
    let usage = BindingUse::Linear if isLinear(ty) else BindingUse::Affine;
    set env.symbols[env.len] = TrackedSymbol { id: sym.id, name: sym.name, node: sym.node, usage };
    set env.available |= (1 as u64) << (env.len as u64);
    set env.len += 1;
}

/// Mark a tracked binding as uninitialized.

    let index = findLinearBinding(env, sym.id) else return;
    set env.available &= ~((1 as u64) << (index as u64));
}

/// Require exact-use bindings introduced after `start` to be consumed.
unsafe fn finishLinearScope 'arena 'checking (
fn finishLinearScope 'arena 'checking (
    checker: &mut LinearChecker 'arena 'checking,
    env: &mut LinearEnv,
    start: u32,
) throws (ResolveError) where 'arena: 'checking {
    if not env.terminated {
        for i in start..env.len {
            if linearBindingAvailable(env, i) {
                let sym = env.symbols[i].symbol;
                let case SymbolData::Value { type: ty, .. } = sym.data
                    else panic "finishLinearScope: expected value symbol";
                if isLinear(ty) {
                let sym = env.symbols[i];
                if sym.usage == BindingUse::Linear {
                    throw emitError(
                        checker.resolver,
                        sym.node,
                        ErrorKind::LinearNotConsumed(sym.name),
                    );

    set env.available &= ~((1 as u64) << (index as u64));
}

/// Merge ownership availability across two live branches.
/// Validate both inputs before writing to an output that can alias either input.
unsafe fn joinLinearBranches 'arena 'checking (
fn joinLinearBranches 'arena 'checking (
    checker: &mut LinearChecker 'arena 'checking,
    env: &mut LinearEnv,
    left: &LinearEnv,
    right: &LinearEnv,
    node: *ast::Node,

    }
    assert left.len == right.len, "joinLinearBranches: scope mismatch";
    let mut available = left.available;
    for i in 0..left.len {
        if linearBindingAvailable(left, i) <> linearBindingAvailable(right, i) {
            let sym = left.symbols[i].symbol;
            let case SymbolData::Value { type: ty, .. } = sym.data
                else panic "joinLinearBranches: expected value symbol";
            if isLinear(ty) {
            let sym = left.symbols[i];
            if sym.usage == BindingUse::Linear {
                throw emitError(
                    checker.resolver,
                    node,
                    ErrorKind::LinearBranchMismatch(sym.name),
                );

    set env.available = available;
    set env.regionalLoans = regionalLoans;
}

/// Require all available exact-use bindings to be consumed at a function exit.
unsafe fn finishLinearExit 'arena 'checking (
fn finishLinearExit 'arena 'checking (
    checker: &mut LinearChecker 'arena 'checking,
    env: &mut LinearEnv,
) throws (ResolveError) where 'arena: 'checking {
    if env.terminated {
        return;
    }
    for i in 0..env.len {
        if linearBindingAvailable(env, i) {
            let sym = env.symbols[i].symbol;
            let case SymbolData::Value { type: ty, .. } = sym.data
                else panic "finishLinearExit: expected value symbol";
            if isLinear(ty) {
            let sym = env.symbols[i];
            if sym.usage == BindingUse::Linear {
                throw emitError(
                    checker.resolver,
                    sym.node,
                    ErrorKind::LinearNotConsumed(sym.name),
                );

    set checker.loopBreakSeen[depth] = false;
    set checker.loopDepth += 1;
}

/// Require a repeated body's outer bindings to match its entry state.
unsafe fn checkLinearLoopBackEdge 'arena 'checking (
fn checkLinearLoopBackEdge 'arena 'checking (
    checker: &mut LinearChecker 'arena 'checking,
    env: &LinearEnv,
    node: *ast::Node,
) throws (ResolveError) where 'arena: 'checking {
    if env.terminated {

    let mark = checker.loopMarks[depth];
    let entryAvailable = checker.loopAvailable[depth];
    for i in 0..mark {
        let bit = (1 as u64) << (i as u64);
        if (env.available & bit) <> (entryAvailable & bit) {
            let sym = env.symbols[i].symbol;
            let sym = env.symbols[i];
            throw emitError(
                checker.resolver,
                node,
                ErrorKind::LinearBranchMismatch(sym.name),
            );

    set checker.loopExitAvailable[depth] = env.available;
    set checker.loopHasNaturalExit[depth] = true;
}

/// Require a break exit to agree with every other exit from this loop.
unsafe fn checkLinearLoopBreak 'arena 'checking (
fn checkLinearLoopBreak 'arena 'checking (
    checker: &mut LinearChecker 'arena 'checking,
    env: &LinearEnv,
    node: *ast::Node,
) throws (ResolveError) where 'arena: 'checking {
    assert checker.loopDepth > 0, "linear loop break outside loop";

    if checker.loopHasNaturalExit[depth] or checker.loopBreakSeen[depth] {
        let expected = checker.loopExitAvailable[depth];
        for i in 0..mark {
            let bit = (1 as u64) << (i as u64);
            if (env.available & bit) <> (expected & bit) {
                let sym = env.symbols[i].symbol;
                let sym = env.symbols[i];
                throw emitError(
                    checker.resolver,
                    node,
                    ErrorKind::LinearBranchMismatch(sym.name),
                );

            }
            case ast::ProngArm::Else => {}
        }
        if prong.guard <> nil {
            for i in bindingsStart..branch.len {
                let sym = branch.symbols[i].symbol;
                let case SymbolData::Value { type: ty, .. } = sym.data
                    else panic "checkLinearMatch: expected value symbol";
                if isLinear(ty) {
                let sym = branch.symbols[i];
                if sym.usage == BindingUse::Linear {
                    throw emitError(checker.resolver, prongNode, ErrorKind::LinearDiscard);
                }
            }
        }
        if let guard = prong.guard {

897	897		Place,
898	898		/// Evaluate a place prefix after checking the complete place.
899	899		Locate,
900	900		}
901	901
902		-	/// Symbol identity and storage retained for ownership diagnostics.
	902	+	/// Consumption rule for a tracked move-only binding.
	903	+	union BindingUse: Copy {
	904	+	/// The binding can be consumed at most once.
	905	+	Affine,
	906	+	/// The binding must be consumed exactly once.
	907	+	Linear,
	908	+	}
	909	+
	910	+	/// Resolved binding metadata retained for ownership checks and diagnostics.
903	911		record TrackedSymbol: Copy {
904	912		/// Resolver-local symbol identity.
905	913		id: u32,
906		-	/// Symbol storage used to report ownership errors.
907		-	symbol: *unsafe mut Symbol,
	914	+	/// Source name used in ownership diagnostics.
	915	+	name: *[u8],
	916	+	/// Declaration used to locate an unconsumed binding.
	917	+	node: *ast::Node,
	918	+	/// Consumption rule fixed before ownership analysis.
	919	+	usage: BindingUse,
908	920		}
909	921
910	922		/// Per-control-flow-path ownership state.
911	923		/// Read only the initialized symbol prefix below `len`.
912	924		record LinearEnv: Copy {
913	925		/// Active full-region loans, indexed by the checker's regional loan table.
914	926		regionalLoans: u64,
915		-	/// Symbol identities and pointers. Entries below `len` are initialized.
	927	+	/// Resolved binding metadata. Entries below `len` are initialized.
916	928		symbols: [TrackedSymbol; MAX_LINEAR_BINDINGS],
917	929		/// Bit set for each binding that remains available.
918	930		available: u64,
919	931		/// Number of initialized entries in `symbols`.
920	932		len: u32,

9915	9927		return;
9916	9928		}
9917	9929		if env.len >= MAX_LINEAR_BINDINGS {
9918	9930		throw emitError(checker.resolver, node, ErrorKind::Internal);
9919	9931		}
9920		-	set env.symbols[env.len] = TrackedSymbol { id: sym.id, symbol: sym };
	9932	+	let usage = BindingUse::Linear if isLinear(ty) else BindingUse::Affine;
	9933	+	set env.symbols[env.len] = TrackedSymbol { id: sym.id, name: sym.name, node: sym.node, usage };
9921	9934		set env.available \|= (1 as u64) << (env.len as u64);
9922	9935		set env.len += 1;
9923	9936		}
9924	9937
9925	9938		/// Mark a tracked binding as uninitialized.

9928	9941		let index = findLinearBinding(env, sym.id) else return;
9929	9942		set env.available &= ~((1 as u64) << (index as u64));
9930	9943		}
9931	9944
9932	9945		/// Require exact-use bindings introduced after `start` to be consumed.
9933		-	unsafe fn finishLinearScope 'arena 'checking (
	9946	+	fn finishLinearScope 'arena 'checking (
9934	9947		checker: &mut LinearChecker 'arena 'checking,
9935	9948		env: &mut LinearEnv,
9936	9949		start: u32,
9937	9950		) throws (ResolveError) where 'arena: 'checking {
9938	9951		if not env.terminated {
9939	9952		for i in start..env.len {
9940	9953		if linearBindingAvailable(env, i) {
9941		-	let sym = env.symbols[i].symbol;
9942		-	let case SymbolData::Value { type: ty, .. } = sym.data
9943		-	else panic "finishLinearScope: expected value symbol";
9944		-	if isLinear(ty) {
	9954	+	let sym = env.symbols[i];
	9955	+	if sym.usage == BindingUse::Linear {
9945	9956		throw emitError(
9946	9957		checker.resolver,
9947	9958		sym.node,
9948	9959		ErrorKind::LinearNotConsumed(sym.name),
9949	9960		);

9983	9994		set env.available &= ~((1 as u64) << (index as u64));
9984	9995		}
9985	9996
9986	9997		/// Merge ownership availability across two live branches.
9987	9998		/// Validate both inputs before writing to an output that can alias either input.
9988		-	unsafe fn joinLinearBranches 'arena 'checking (
	9999	+	fn joinLinearBranches 'arena 'checking (
9989	10000		checker: &mut LinearChecker 'arena 'checking,
9990	10001		env: &mut LinearEnv,
9991	10002		left: &LinearEnv,
9992	10003		right: &LinearEnv,
9993	10004		node: *ast::Node,

10007	10018		}
10008	10019		assert left.len == right.len, "joinLinearBranches: scope mismatch";
10009	10020		let mut available = left.available;
10010	10021		for i in 0..left.len {
10011	10022		if linearBindingAvailable(left, i) <> linearBindingAvailable(right, i) {
10012		-	let sym = left.symbols[i].symbol;
10013		-	let case SymbolData::Value { type: ty, .. } = sym.data
10014		-	else panic "joinLinearBranches: expected value symbol";
10015		-	if isLinear(ty) {
	10023	+	let sym = left.symbols[i];
	10024	+	if sym.usage == BindingUse::Linear {
10016	10025		throw emitError(
10017	10026		checker.resolver,
10018	10027		node,
10019	10028		ErrorKind::LinearBranchMismatch(sym.name),
10020	10029		);

10027	10036		set env.available = available;
10028	10037		set env.regionalLoans = regionalLoans;
10029	10038		}
10030	10039
10031	10040		/// Require all available exact-use bindings to be consumed at a function exit.
10032		-	unsafe fn finishLinearExit 'arena 'checking (
	10041	+	fn finishLinearExit 'arena 'checking (
10033	10042		checker: &mut LinearChecker 'arena 'checking,
10034	10043		env: &mut LinearEnv,
10035	10044		) throws (ResolveError) where 'arena: 'checking {
10036	10045		if env.terminated {
10037	10046		return;
10038	10047		}
10039	10048		for i in 0..env.len {
10040	10049		if linearBindingAvailable(env, i) {
10041		-	let sym = env.symbols[i].symbol;
10042		-	let case SymbolData::Value { type: ty, .. } = sym.data
10043		-	else panic "finishLinearExit: expected value symbol";
10044		-	if isLinear(ty) {
	10050	+	let sym = env.symbols[i];
	10051	+	if sym.usage == BindingUse::Linear {
10045	10052		throw emitError(
10046	10053		checker.resolver,
10047	10054		sym.node,
10048	10055		ErrorKind::LinearNotConsumed(sym.name),
10049	10056		);

10517	10524		set checker.loopBreakSeen[depth] = false;
10518	10525		set checker.loopDepth += 1;
10519	10526		}
10520	10527
10521	10528		/// Require a repeated body's outer bindings to match its entry state.
10522		-	unsafe fn checkLinearLoopBackEdge 'arena 'checking (
	10529	+	fn checkLinearLoopBackEdge 'arena 'checking (
10523	10530		checker: &mut LinearChecker 'arena 'checking,
10524	10531		env: &LinearEnv,
10525	10532		node: *ast::Node,
10526	10533		) throws (ResolveError) where 'arena: 'checking {
10527	10534		if env.terminated {

10533	10540		let mark = checker.loopMarks[depth];
10534	10541		let entryAvailable = checker.loopAvailable[depth];
10535	10542		for i in 0..mark {
10536	10543		let bit = (1 as u64) << (i as u64);
10537	10544		if (env.available & bit) <> (entryAvailable & bit) {
10538		-	let sym = env.symbols[i].symbol;
	10545	+	let sym = env.symbols[i];
10539	10546		throw emitError(
10540	10547		checker.resolver,
10541	10548		node,
10542	10549		ErrorKind::LinearBranchMismatch(sym.name),
10543	10550		);

10553	10560		set checker.loopExitAvailable[depth] = env.available;
10554	10561		set checker.loopHasNaturalExit[depth] = true;
10555	10562		}
10556	10563
10557	10564		/// Require a break exit to agree with every other exit from this loop.
10558		-	unsafe fn checkLinearLoopBreak 'arena 'checking (
	10565	+	fn checkLinearLoopBreak 'arena 'checking (
10559	10566		checker: &mut LinearChecker 'arena 'checking,
10560	10567		env: &LinearEnv,
10561	10568		node: *ast::Node,
10562	10569		) throws (ResolveError) where 'arena: 'checking {
10563	10570		assert checker.loopDepth > 0, "linear loop break outside loop";

10567	10574		if checker.loopHasNaturalExit[depth] or checker.loopBreakSeen[depth] {
10568	10575		let expected = checker.loopExitAvailable[depth];
10569	10576		for i in 0..mark {
10570	10577		let bit = (1 as u64) << (i as u64);
10571	10578		if (env.available & bit) <> (expected & bit) {
10572		-	let sym = env.symbols[i].symbol;
	10579	+	let sym = env.symbols[i];
10573	10580		throw emitError(
10574	10581		checker.resolver,
10575	10582		node,
10576	10583		ErrorKind::LinearBranchMismatch(sym.name),
10577	10584		);

10666	10673		}
10667	10674		case ast::ProngArm::Else => {}
10668	10675		}
10669	10676		if prong.guard <> nil {
10670	10677		for i in bindingsStart..branch.len {
10671		-	let sym = branch.symbols[i].symbol;
10672		-	let case SymbolData::Value { type: ty, .. } = sym.data
10673		-	else panic "checkLinearMatch: expected value symbol";
10674		-	if isLinear(ty) {
	10678	+	let sym = branch.symbols[i];
	10679	+	if sym.usage == BindingUse::Linear {
10675	10680		throw emitError(checker.resolver, prongNode, ErrorKind::LinearDiscard);
10676	10681		}
10677	10682		}
10678	10683		}
10679	10684		if let guard = prong.guard {