diff --git a/docs/thesis.md b/docs/thesis.md index 277436f..89d4afd 100644 --- a/docs/thesis.md +++ b/docs/thesis.md @@ -45,6 +45,13 @@ Alias/Move 모델 (철학 1,3에서 파생 — 언어 전체의 토대): 미해제는 검사하지 않는다 (오용 금지, 누수 허용). linear 검사와 해제 보장은 v1 과제 - v0에 first-class reference는 없다. mutable 데이터는 소유 변수를 통해서만 변경 +- 클로저는 mut 바인딩을 capture할 수 없다. 참조가 없으므로 별칭을 만들 수도, + 조용히 복사할 수도 없기 때문이다. spawn 클로저 제한은 이 일반 규칙의 특수 사례다 +- v0에 부분 move는 없다. 필드 접근은 빌림이고 결과도 빌린 값이다 + ※ struct에서 affine 필드만 꺼내 가려면 부분 move 상태 추적이 필요한데, + 그 복잡도는 v0가 사려는 것이 아니다. 필요하면 통째로 own으로 받는다 +- 외부 타입은 affine임을 증명할 수 없으므로 copyable로 본다. + 모르는 것을 위반이라고 말하지 않는다 — 모듈 로딩이 생기면 판정된다 - 공유는 deep immutable 값만 가능 (내부 가변성 타입은 v0에 없음) 근거: "safe code에 data race 없음"은 spawn만 막아서 성립하지 않는다. closure, channel, container, 인자/반환 전 경로에서 mutable alias가 없어야 하며, 값 의미론 @@ -107,8 +114,8 @@ Affinity 전이 (보안 주장의 필수 전제): - structured concurrency만 허용: 태스크 수명 = 블록 구조 (locality) - 데이터 경쟁은 격리로: mutable은 단일 소유, channel로 소유권 이동, 공유는 deep immutable만 (borrow checker는 complexity budget 초과) -- spawn closure는 by-move capture 또는 immutable capture만 허용. - mutable 참조 capture는 문법적으로 금지 +- spawn closure는 by-move capture 또는 immutable capture만 허용 + (Alias/Move 모델의 mut capture 금지가 그대로 적용된다) - spawn은 primitive가 아니라 TaskScope capability의 메서드다. effect spawn은 아래 "정적/동적 층 분리"대로 그 타입에 묶인다 (PaymentGateway.refund와 동형) diff --git a/lib/driver.ml b/lib/driver.ml index 8d5b56b..e7f6b8b 100644 --- a/lib/driver.ml +++ b/lib/driver.ml @@ -69,19 +69,27 @@ let typecheck (file : string) : (unit, error list) result = { file; line = e.pos.line; col = e.pos.col; message = e.msg }) rerrors) | [] -> ( - match Typecheck.check m with + let terrors = + List.map + (fun (e : Typecheck.error) -> + { file; line = e.pos.line; col = e.pos.col; message = e.msg }) + (Typecheck.check m) + in + (* move/affinity는 타입·effect와 달리 별도 순회다. 소유하는 성질이 + 다르고 해소를 공유할 지점도 없기 때문이다. *) + let merrors = + List.map + (fun (e : Move.error) -> + { file; line = e.pos.line; col = e.pos.col; message = e.msg }) + (Move.check m) + in + match + List.sort + (fun a b -> compare (a.line, a.col) (b.line, b.col)) + (terrors @ merrors) + with | [] -> Ok () - | terrors -> - Error - (List.map - (fun (e : Typecheck.error) -> - { - file; - line = e.pos.line; - col = e.pos.col; - message = e.msg; - }) - terrors))) + | errors -> Error errors)) let check (files : string list) : (unit, error list) result = match files with @@ -94,21 +102,7 @@ let check (files : string list) : (unit, error list) result = files |> List.concat in - if errors <> [] then Error errors - else - (* effect 검사까지는 통과했다. 통과했다고 말하지 않는다 — 파이프라인의 - 나머지가 아직 없으므로 검사되지 않은 것이다. *) - Error - (List.map - (fun f -> - { - file = f; - line = 0; - col = 0; - message = - "effect/capability 검사까지 통과. move/affinity 검사가 아직 구현되지 않았습니다"; - }) - files) + if errors <> [] then Error errors else Ok () let run (file : string) : (unit, error list) result = Error [ { file; line = 0; col = 0; message = "interpreter가 아직 구현되지 않았습니다" } ] diff --git a/lib/move.ml b/lib/move.ml new file mode 100644 index 0000000..8483e6b --- /dev/null +++ b/lib/move.ml @@ -0,0 +1,471 @@ +(* move / affinity 검사. + + 보안 정리 (ii) — safe code에서 capability는 복제·위조되지 않는다 — 를 코드로 + 닫는 단계다. 검사는 전부 함수 로컬 데이터플로우다. 전역 분석이 없다. + + affinity의 뿌리는 capability다. capability를 필드로 가진 타입은 전이적으로 + affine이고(철학 3), 이 전이가 없으면 wrapper 하나를 복사해 capability가 + 사실상 복제된다. + + 외부 타입은 affine임을 증명할 수 없으므로 copyable로 본다 — 모르는 것을 + 위반이라고 말하지 않는다. 그래서 이 검사를 시험하려면 자원 타입을 모듈 + 안에서 정의해야 한다 (samples/05). *) + +open Ast + +type error = { pos : Token.pos; msg : string } + +(* 값이 무엇인가: 소유한 affine 값인가, 빌린 값인가. 둘은 직교한다. *) +type vinfo = { v_affine : bool; v_use : bool } + +let v_copy = { v_affine = false; v_use = false } + +type binding = { + b_id : int; + b_name : string; + b_affine : bool; + b_use : bool; + b_mut : bool; + b_depth : int; +} + +type fninfo = { f_params : param list; f_ret : Ast.ty option } + +type state = { + aff : (string, bool) Hashtbl.t; + fns : (string, fninfo) Hashtbl.t; + meths : (string, (string * fninfo) list) Hashtbl.t; + mutable scopes : binding list list; + moved : (int, Token.pos) Hashtbl.t; + mutable next_id : int; + mutable depth : int; + (* 클로저 프레임: (프레임 깊이, 잡아온 바깥 바인딩). 중첩 클로저를 위해 스택 *) + mutable frames : (int * binding list ref) list; + mutable errors : error list; +} + +let err st pos msg = st.errors <- { pos; msg } :: st.errors + +(* ------------------------------------------------------------------ *) +(* affinity 유도 *) +(* ------------------------------------------------------------------ *) + +let builtin_containers = [ "List"; "Option"; "Result" ] + +let rec ty_affine st (t : Ast.ty) = + match t with + | T_fn { affine; _ } -> affine + | T_named { name; args; _ } -> + let self = + match Hashtbl.find_opt st.aff name with Some b -> b | None -> false + in + let arg_affine = + List.exists + (function TA_ty t -> ty_affine st t | TA_eff _ -> false) + args + in + self || (List.mem name builtin_containers && arg_affine) || arg_affine + +(* capability가 뿌리다. struct/enum은 필드에서 전이된다. 상호 재귀 타입을 위해 + 변화가 없을 때까지 돈다. *) +let derive_affinity st (m : modul) = + List.iter + (fun it -> + match it with + | I_capability { name; _ } -> Hashtbl.replace st.aff name true + | I_struct { name; _ } -> Hashtbl.replace st.aff name false + | I_enum { name; _ } -> Hashtbl.replace st.aff name false + | _ -> ()) + m.items; + let changed = ref true in + while !changed do + changed := false; + List.iter + (fun it -> + let update name affine = + if affine && Hashtbl.find_opt st.aff name <> Some true then ( + Hashtbl.replace st.aff name true; + changed := true) + in + match it with + | I_struct { name; fields; _ } -> + update name (List.exists (fun f -> ty_affine st f.f_ty) fields) + | I_enum { name; variants; _ } -> + update name + (List.exists + (fun v -> List.exists (ty_affine st) v.v_args) + variants) + | _ -> ()) + m.items + done; + (* copyable 선언과 affine 필드는 공존할 수 없다 *) + List.iter + (fun it -> + match it with + | I_struct { copyable = true; name; fields; pos; _ } -> + List.iter + (fun f -> + if ty_affine st f.f_ty then + err st f.f_pos + (Printf.sprintf "%s은(는) copyable로 선언되었지만 %s 필드가 affine입니다" + name f.f_name)) + fields; + ignore pos + | _ -> ()) + m.items + +(* ------------------------------------------------------------------ *) +(* 스코프 *) +(* ------------------------------------------------------------------ *) + +let push st = st.scopes <- [] :: st.scopes +let pop st = match st.scopes with _ :: r -> st.scopes <- r | [] -> () + +let add st name ~affine ~use ~mut_ = + st.next_id <- st.next_id + 1; + let b = + { + b_id = st.next_id; + b_name = name; + b_affine = affine; + b_use = use; + b_mut = mut_; + b_depth = st.depth; + } + in + (match st.scopes with + | s :: r -> st.scopes <- (b :: s) :: r + | [] -> st.scopes <- [ [ b ] ]); + b + +let find st name = + let rec go = function + | [] -> None + | s :: r -> ( + match List.find_opt (fun b -> b.b_name = name) s with + | Some b -> Some b + | None -> go r) + in + go st.scopes + +(* 클로저 안에서 바깥 바인딩을 건드리면 capture다. 프레임마다 기록한다. *) +let note_capture st b = + List.iter + (fun (fdepth, acc) -> + if b.b_depth < fdepth && not (List.exists (fun x -> x.b_id = b.b_id) !acc) + then acc := b :: !acc) + st.frames + +(* ------------------------------------------------------------------ *) +(* 분기 병합 — 보수적 합집합 *) +(* ------------------------------------------------------------------ *) + +let snapshot st = Hashtbl.copy st.moved + +let restore st snap = + Hashtbl.reset st.moved; + Hashtbl.iter (fun k v -> Hashtbl.replace st.moved k v) snap + +let merge st snaps = + (* 한 분기에서라도 moved면 병합 지점 이후 moved *) + Hashtbl.reset st.moved; + List.iter + (fun snap -> + Hashtbl.iter + (fun k v -> + if not (Hashtbl.mem st.moved k) then Hashtbl.replace st.moved k v) + snap) + snaps + +(* ------------------------------------------------------------------ *) +(* 식 *) +(* ------------------------------------------------------------------ *) + +type ctx = Borrow | Move of string (* 어디로 옮겨가는지 — 진단에 쓴다 *) + +let rec walk st (ctx : ctx) (e : expr) : vinfo = + match e with + | E_lit _ -> v_copy + | E_ident (n, pos) -> ( + match find st n with + | None -> v_copy + | Some b -> + note_capture st b; + (match Hashtbl.find_opt st.moved b.b_id with + | Some mp -> + err st pos + (Printf.sprintf "%s은(는) 이미 move되었습니다 (%d:%d에서 소비)" n + mp.Token.line mp.Token.col) + | None -> ()); + (match ctx with + | Borrow -> () + | Move where -> + if b.b_use then + err st pos + (Printf.sprintf "%s은(는) 빌린 값이라 %s 없습니다 (own으로 받아야 합니다)" n + where) + else if b.b_affine then Hashtbl.replace st.moved b.b_id pos); + { v_affine = b.b_affine; v_use = b.b_use }) + | E_list (xs, _) -> + let infos = List.map (walk st (Move "컨테이너에 넣을 수")) xs in + { v_affine = List.exists (fun i -> i.v_affine) infos; v_use = false } + | E_struct { name; fields; _ } -> + List.iter (fun (_, e) -> ignore (walk st (Move "struct에 저장할 수") e)) fields; + { + v_affine = + (match Hashtbl.find_opt st.aff name with + | Some b -> b + | None -> false); + v_use = false; + } + | E_closure c -> ( + let r = walk_closure st c in + (* use의 전염: 빌린 값을 capture한 클로저는 그 자체가 빌린 값이라 + 소유를 가져가는 자리로 갈 수 없다. 별도의 nonescaping 개념 없이 + use 규칙 하나로 닫힌다. *) + match ctx with + | Move where when r.v_use -> + err st c.cl_pos + (Printf.sprintf "빌린 값을 capture한 클로저는 %s 없습니다 (use 값은 탈출하지 못합니다)" + where); + r + | _ -> r) + | E_if { cond; then_; else_; _ } -> + ignore (walk st Borrow cond); + let before = snapshot st in + let t1 = walk_block st ctx then_ in + let s1 = snapshot st in + restore st before; + let t2 = match else_ with None -> v_copy | Some e -> walk st ctx e in + let s2 = snapshot st in + merge st [ s1; s2 ]; + { v_affine = t1.v_affine || t2.v_affine; v_use = t1.v_use || t2.v_use } + | E_match { scrutinee; arms; _ } -> + let sinfo = walk st Borrow scrutinee in + let before = snapshot st in + let results = + List.map + (fun a -> + restore st before; + push st; + bind_pattern st sinfo a.arm_pat; + let r = walk st ctx a.arm_body in + pop st; + (r, snapshot st)) + arms + in + if results <> [] then merge st (List.map snd results); + { + v_affine = List.exists (fun (r, _) -> r.v_affine) results; + v_use = List.exists (fun (r, _) -> r.v_use) results; + } + | E_scope { name; parent; body; _ } -> + ignore (walk st Borrow (E_ident (parent, Token.{ line = 0; col = 0 }))); + push st; + (* 자식 TaskScope는 second-class다 — 블록 밖으로 나갈 수 없다 *) + ignore (add st name ~affine:true ~use:true ~mut_:false); + let r = walk_block st ctx body in + pop st; + r + | E_block b -> + push st; + let r = walk_block st ctx b in + pop st; + r + | E_call { callee; args; pos } -> walk_call st callee args pos + | E_field { obj; _ } -> + (* v0에 부분 move는 없다. 필드 접근은 빌림이고 결과도 빌린 값이다. *) + let o = walk st Borrow obj in + if o.v_affine || o.v_use then { v_affine = true; v_use = true } + else v_copy + | E_inst { callee; _ } -> walk st Borrow callee + | E_try { inner; _ } -> walk st ctx inner + | E_unary { operand; _ } -> walk st Borrow operand + | E_binary { lhs; rhs; _ } -> + ignore (walk st Borrow lhs); + ignore (walk st Borrow rhs); + v_copy + +and bind_pattern st (info : vinfo) p = + match p with + | P_wild _ | P_lit _ -> () + | P_bind (n, _) -> + ignore (add st n ~affine:info.v_affine ~use:info.v_use ~mut_:false) + | P_ctor { args; _ } -> List.iter (bind_pattern st info) args + +and walk_block st ctx (b : block) : vinfo = + let rec go = function + | [] -> v_copy + | [ S_expr e ] -> walk st ctx e (* 꼬리 식은 블록의 값이다 *) + | s :: rest -> + walk_stmt st s; + go rest + in + go b.stmts + +and walk_stmt st = function + | S_let { mut_; pat; value; _ } -> + let info = walk st (Move "다른 이름에 묶을 수") value in + let rec bind p = + match p with + | P_bind (n, _) -> + ignore (add st n ~affine:info.v_affine ~use:info.v_use ~mut_) + | P_ctor { args; _ } -> List.iter bind args + | _ -> () + in + bind pat + | S_return { value; _ } -> ( + match value with + | None -> () + | Some e -> ignore (walk st (Move "반환할 수") e)) + | S_assign { place; value; _ } -> + ignore (walk st (Move "대입할 수") value); + ignore (walk st Borrow place) + | S_expr e -> ignore (walk st Borrow e) + +(* 클로저: 무엇을 잡아왔는지가 클로저 자신의 성질을 정한다 (전이 규칙) *) +and walk_closure st (c : closure) : vinfo = + st.depth <- st.depth + 1; + let acc = ref [] in + st.frames <- (st.depth, acc) :: st.frames; + push st; + List.iter + (fun (n, ann) -> + let affine = match ann with Some t -> ty_affine st t | None -> false in + ignore (add st n ~affine ~use:false ~mut_:false)) + c.cl_params; + ignore (walk_block st (Move "반환할 수") c.cl_body); + pop st; + st.frames <- List.tl st.frames; + st.depth <- st.depth - 1; + let captured = !acc in + let affine = ref false and use_ = ref false in + List.iter + (fun b -> + if b.b_mut then + err st c.cl_pos + (Printf.sprintf + "클로저는 mut 바인딩 %s을(를) capture할 수 없습니다 (v0에 참조가 없으므로 별칭도 복사도 만들지 \ + 않는다)" + b.b_name); + if b.b_use then use_ := true; + if b.b_affine && not b.b_use then ( + (* by-move capture: 바깥에서는 여기서 소비된다 *) + affine := true; + if not (Hashtbl.mem st.moved b.b_id) then + Hashtbl.replace st.moved b.b_id c.cl_pos)) + captured; + { v_affine = !affine; v_use = !use_ } + +and walk_call st callee args pos = + let info = callee_info st callee in + ignore (walk st Borrow callee); + let params = match info with Some f -> f.f_params | None -> [] in + List.iteri + (fun i a -> + let p = List.nth_opt params i in + let own = match p with Some p -> p.p_own | None -> false in + let pty = Option.map (fun p -> p.p_ty) p in + let ctx = if own then Move "다른 함수에 넘길 수" else Borrow in + let got = walk st ctx a in + (* callable affinity: affine 클로저를 fn 자리에 넘길 수 없다 *) + match pty with + | Some (T_fn { affine = false; _ }) when got.v_affine && not got.v_use -> + err st pos + "affine 값을 capture한 클로저는 fn 자리에 넘길 수 없습니다 (affine fn이어야 합니다)" + | _ -> ()) + args; + match info with + | Some { f_ret = Some t; _ } -> { v_affine = ty_affine st t; v_use = false } + | _ -> v_copy + +and callee_info st callee = + match callee with + | E_ident (n, _) when find st n = None -> Hashtbl.find_opt st.fns n + | E_inst { callee = E_ident (n, _); _ } when find st n = None -> + Hashtbl.find_opt st.fns n + | E_field { obj = E_ident (o, _); name; _ } -> ( + match find st o with + | Some _ -> ( + (* 값의 메서드: 타입을 모르면 넘어간다. capability 메서드는 아래에서 *) + match + Hashtbl.fold + (fun _ methods acc -> + match acc with + | Some _ -> acc + | None -> List.assoc_opt name methods) + st.meths None + with + | Some f -> Some f + | None -> None) + | None -> None) + | _ -> None + +(* ------------------------------------------------------------------ *) +(* 선언 *) +(* ------------------------------------------------------------------ *) + +let check_fn st (d : fn_decl) = + match d.fn_body with + | None -> () + | Some body -> + st.scopes <- []; + Hashtbl.reset st.moved; + st.depth <- 0; + st.frames <- []; + push st; + List.iter + (fun p -> + let affine = ty_affine st p.p_ty in + (* 무표기 = 빌림. own만이 소유 이전이다. *) + let use_ = affine && not p.p_own in + ignore (add st p.p_name ~affine ~use:use_ ~mut_:p.p_mut)) + d.fn_params; + let r = walk_block st (Move "반환할 수") body in + (match d.fn_ret with + | Some (T_fn { affine = false; _ }) when r.v_affine && not r.v_use -> + err st d.fn_pos + (Printf.sprintf + "%s이(가) affine 값을 capture한 클로저를 fn 타입으로 반환합니다 (affine fn이어야 합니다)" + d.fn_name) + | _ -> ()); + pop st + +let check (m : modul) : error list = + let st = + { + aff = Hashtbl.create 16; + fns = Hashtbl.create 16; + meths = Hashtbl.create 16; + scopes = []; + moved = Hashtbl.create 16; + next_id = 0; + depth = 0; + frames = []; + errors = []; + } + in + derive_affinity st m; + List.iter + (fun it -> + match it with + | I_fn { decl; _ } -> + Hashtbl.replace st.fns decl.fn_name + { f_params = decl.fn_params; f_ret = decl.fn_ret } + | I_capability { name; methods; _ } -> + Hashtbl.replace st.meths name + (List.map + (fun d -> + (d.fn_name, { f_params = d.fn_params; f_ret = d.fn_ret })) + methods) + | _ -> ()) + m.items; + List.iter + (fun it -> match it with I_fn { decl; _ } -> check_fn st decl | _ -> ()) + m.items; + List.sort + (fun a b -> + compare + (a.pos.Token.line, a.pos.Token.col) + (b.pos.Token.line, b.pos.Token.col)) + (List.rev st.errors) diff --git a/samples/05_move_errors.cool b/samples/05_move_errors.cool index 000a3d7..f104902 100644 --- a/samples/05_move_errors.cool +++ b/samples/05_move_errors.cool @@ -1,26 +1,38 @@ -// 05. 컴파일 에러가 나야 하는 코드 +// 05. move / affinity 검사기가 거부해야 하는 코드 // -// 각 함수는 주석에 적힌 진단 하나를 정확히 내야 한다. -// 체커가 생기면 그대로 테스트 케이스가 된다. +// 09, 10과 같은 이유로 외부 타입이 하나도 없다. affinity의 뿌리는 capability라 +// 자원 타입을 이 파일에서 정의해야 검사기가 affine임을 알 수 있다. +// 외부 타입은 affine임을 증명할 수 없으므로 copyable로 취급된다. -// close는 파일을 소비한다: own 유표기 +pub capability File { + fn size() -> Int +} + +pub capability Gateway { + fn refund(id: Int) effects {Gateway.refund} +} + +pub capability Registry { + fn add(h: fn()) effects {Registry.add} +} + +// 파일을 소비하는 함수: own 유표기 pub fn close(own f: File) effects {File.close} -// [E-move-after-move] affine 값의 이중 소비 -pub fn double_close(own f: File) effects {File.close} { +// 빌리기만 하는 함수: 무표기 +pub fn size_of(f: File) -> Int { + f.size() +} + +// --- 통과해야 하는 것 --- + +pub fn use_then_close(own f: File) effects {File.close} -> Int { + let n = size_of(f) close(f) - close(f) // ERROR: f는 이미 move됨 (앞줄에서 소비) + n } -// [E-move-join] 분기 병합은 보수적 합집합 -pub fn conditional_close(own f: File, c: Bool) effects {File.close} { - if c { - close(f) - } - close(f) // ERROR: f는 이 분기에서 move됨 (조건부 소비) -} - -// 정당한 형태 — 양쪽 분기에서 소비하면 통과해야 한다. +// 양쪽 분기에서 소비하면 통과한다 pub fn both_branches_close(own f: File, c: Bool) effects {File.close} { if c { close(f) @@ -29,48 +41,75 @@ pub fn both_branches_close(own f: File, c: Bool) effects {File.close} { } } +// 빌린 값을 다른 빌림 자리로 넘기는 것은 복제가 아니다 +pub fn borrow_twice(f: File) -> Int { + size_of(f) + size_of(f) +} + +// affine 값을 capture한 클로저는 affine fn이다 +pub fn deferred_close(own f: File) -> affine fn() effects {File.close} { + fn() { close(f) } +} + +// --- 여기서부터 전부 오류다 --- + +// [E-move-after-move] affine 값의 이중 소비 +pub fn double_close(own f: File) effects {File.close} { + close(f) + close(f) +} + +// [E-move-join] 분기 병합은 보수적 합집합 +pub fn conditional_close(own f: File, c: Bool) effects {File.close} { + if c { + close(f) + } + close(f) +} + // [E-use-escape] 빌린 값의 반환 -pub fn leak_capability(pay: PaymentGateway) -> PaymentGateway { - pay // ERROR: 빌린 값은 반환할 수 없음 (own이 아니다) +pub fn leak_capability(pay: Gateway) -> Gateway { + pay } // [E-use-escape] 빌린 값의 저장 pub struct Holder { - pay: PaymentGateway, + pay: Gateway, } -pub fn store_capability(pay: PaymentGateway) -> Holder { - Holder { pay: pay } // ERROR: 빌린 값은 struct에 저장할 수 없음 +pub fn store_capability(pay: Gateway) -> Holder { + Holder { pay: pay } } -// [E-use-escape] 빌린 값을 capture한 클로저를 own 자리에 전달 -pub fn register(own handler: fn()) effects {Registry.add} +// [E-use-escape] 빌린 값을 다른 함수에 소유로 넘긴다 +pub fn give_away(f: File) effects {File.close} { + close(f) +} -pub fn escape_via_closure(pay: PaymentGateway) effects {Registry.add} { - register(fn() { pay.refund(OrderId(1)) }) - // ERROR: pay를 capture한 클로저는 빌린 값이며 own 자리에 전달할 수 없음 +// [E-use-escape] 빌린 값을 capture한 클로저를 own 자리에 넘긴다 +pub fn register(own h: fn() effects {Gateway.refund}) effects {Registry.add} + +pub fn escape_via_closure(pay: Gateway) effects {Registry.add} { + register(fn() { pay.refund(1) }) } // [E-affinity-transitive] affine 필드를 가진 타입을 copyable로 선언 pub copyable struct Box { - f: File, // ERROR: affine 필드(File)와 copyable 선언은 공존할 수 없음 + f: File, } -// [E-callable-affinity] affine 값을 capture한 클로저를 fn 위치에 대입 +// [E-callable-affinity] affine 값을 capture한 클로저를 fn 위치에 반환 pub fn misuse_affine_closure(own f: File) -> fn() effects {File.close} { fn() { close(f) } - // ERROR: f를 capture했으므로 타입은 affine fn()이며 fn() 위치에 대입할 수 없음 } -// [E-spawn-capture] spawn 클로저의 mutable capture -pub fn spawn_mutable(sc: TaskScope, mut counter: Int) effects {TaskScope.spawn} { - scope s = sc { - sc.spawn(fn() { counter = counter + 1 }) - // ERROR: spawn 클로저는 mutable 참조를 capture할 수 없음 - } -} - -// [E-effect-undeclared] 선언되지 않은 effect -pub fn silent_write(log: Logger) { - log.write("hi") // ERROR: effect Logger.write가 시그니처에 선언되지 않음 +// [E-closure-mut-capture] 클로저는 mut 바인딩을 capture할 수 없다 +pub fn capture_mut(own f: File, pay: Gateway) + effects {File.close, Registry.add, Gateway.refund} { + let mut counter = 0 + register(fn() { + counter = counter + 1 + pay.refund(counter) + }) + close(f) } diff --git a/samples/README.md b/samples/README.md index ab91c62..a8ba546 100644 --- a/samples/README.md +++ b/samples/README.md @@ -12,7 +12,7 @@ | 02_higher_order_effects | effect 변수, 구문 수준 제한, 명시적 인스턴스화 | | 03_scope_concurrency | TaskScope, 이름 있는 scope, 중첩 시 수명 표현 | | 04_enum_match_interface | enum 정의 본문이 interface surface에 들어가는 경로 | -| 05_move_errors | **에러가 나야 하는** 코드 — 진단 하나씩 | +| 05_move_errors | **move/affinity 검사기가** 거부해야 하는 코드 (자원을 직접 정의) | | 06_affine_closure | callable affinity (fn vs affine fn), own과의 직교성 | | 07_module_interface | interface artifact가 담아야 할 것 전부 | | 08_syntax_errors | **파서가** 거부해야 하는 코드 | @@ -21,13 +21,16 @@ 05, 08, 09, 10은 통과하면 안 되는 파일이다. 각 함수 주석의 `[E-...]` 태그가 기대 진단이며, 넷의 목적이 다르다 — **08은 파서가, 09는 타입 검사기가, -10은 effect 검사기가, 05는 아직 없는 move/affinity 검사가** 거부해야 한다. -단계별로 파일을 나눈 이유는 앞 단계가 첫 오류에서 멈추면 뒤 단계 케이스에 -영영 도달하지 못하기 때문이다. +10은 effect 검사기가, 05는 move/affinity 검사가** 거부해야 한다. 단계별로 +파일을 나눈 이유는 앞 단계가 첫 오류에서 멈추면 뒤 단계 케이스에 영영 +도달하지 못하기 때문이다. -09와 10에는 외부 타입이 하나도 없다. 전부 모듈 안에서 정의되므로 검사기가 -TUnknown으로 빠져나갈 구석이 없다 — 검사기에 이빨이 있는지 보는 파일이다. -10은 capability를 직접 정의해야 메서드의 effect가 알려지므로 특히 그렇다. +05, 09, 10에는 외부 타입이 하나도 없다. 전부 모듈 안에서 정의되므로 검사기가 +빠져나갈 구석이 없다 — 검사기에 이빨이 있는지 보는 파일들이다. 10은 +capability를 직접 정의해야 메서드의 effect가 알려지고, 05는 affinity의 뿌리가 +capability라 자원 타입을 정의해야 affine임이 유도된다. + +01~04, 06, 07은 `cool check`를 통과한다 (exit 0). 파서는 첫 오류에서 멈춘다(오류 복구 미구현). 타입 검사기는 오류를 전부 모은다. diff --git a/test/test_coollang.ml b/test/test_coollang.ml index 3d6bd28..656cf18 100644 --- a/test/test_coollang.ml +++ b/test/test_coollang.ml @@ -580,7 +580,8 @@ let () = Sys.readdir dir |> Array.to_list |> List.filter (fun f -> Filename.check_suffix f ".cool") |> List.filter (fun f -> - f <> "08_syntax_errors.cool" + f <> "05_move_errors.cool" + && f <> "08_syntax_errors.cool" && f <> "09_type_errors.cool" && f <> "10_effect_errors.cool") |> List.sort compare @@ -599,9 +600,12 @@ let () = | Ok () -> check "09는 타입 오류를 내야 한다" false | Error errors -> check "09의 오류를 전부 모은다 (첫 오류에서 멈추지 않는다)" (List.length errors >= 18)); - match Driver.typecheck (Filename.concat dir "10_effect_errors.cool") with + (match Driver.typecheck (Filename.concat dir "10_effect_errors.cool") with | Ok () -> check "10은 effect 오류를 내야 한다" false - | Error errors -> check "10의 effect 오류" (List.length errors >= 6) + | Error errors -> check "10의 effect 오류" (List.length errors >= 6)); + match Driver.typecheck (Filename.concat dir "05_move_errors.cool") with + | Ok () -> check "05는 move 오류를 내야 한다" false + | Error errors -> check "05의 move 오류" (List.length errors >= 9) (* ================================================================== *) (* effect / capability 검사 *) @@ -688,3 +692,128 @@ let () = (type_has (cap ^ "fn f() effects {Db.read} -> Int {\n Db.read(1)\n}") "값을 통해서만") + +(* ================================================================== *) +(* move / affinity 검사 *) +(* ================================================================== *) + +let move_errs src = + List.map (fun (e : Move.error) -> e.msg) (Move.check (parse_ok src)) + +let move_ok src = move_errs src = [] + +let move_has src frag = + List.exists + (fun m -> + let n = String.length frag in + let rec go i = + i + n <= String.length m && (String.sub m i n = frag || go (i + 1)) + in + go 0) + (move_errs src) + +let res = + "capability F {\n\ + \ fn size() -> Int\n\ + }\n\ + fn drop(own f: F)\n\ + fn peek(f: F) -> Int\n" + +(* --- 이중 소비와 분기 병합 --- *) + +let () = + check "빌리기만 하면 여러 번 써도 된다" + (move_ok (res ^ "fn f(x: F) -> Int {\n peek(x) + peek(x)\n}")); + check "이중 소비는 오류" + (move_has (res ^ "fn f(own x: F) {\n drop(x)\n drop(x)\n}") "이미 move"); + check "양쪽 분기에서 소비하면 통과" + (move_ok + (res + ^ "fn f(own x: F, c: Bool) {\n\ + \ if c {\n\ + \ drop(x)\n\ + \ } else {\n\ + \ drop(x)\n\ + \ }\n\ + }")); + check "한 분기에서만 소비해도 병합 이후는 moved (보수적 합집합)" + (move_has + (res + ^ "fn f(own x: F, c: Bool) {\n if c {\n drop(x)\n }\n drop(x)\n}") + "이미 move"); + check "소비한 자리를 진단에 담는다" + (move_has (res ^ "fn f(own x: F) {\n drop(x)\n drop(x)\n}") "에서 소비") + +(* --- 빌린 값은 탈출하지 못한다 --- *) + +let () = + check "빌린 값의 반환" (move_has (res ^ "fn f(x: F) -> F {\n x\n}") "반환할 수 없습니다"); + check "빌린 값을 소유 자리로" (move_has (res ^ "fn f(x: F) {\n drop(x)\n}") "빌린 값이라"); + check "own으로 받으면 넘길 수 있다" (move_ok (res ^ "fn f(own x: F) {\n drop(x)\n}")); + check "빌린 값의 struct 저장" + (move_has + (res ^ "struct H {\n f: F,\n}\nfn g(x: F) -> H {\n H { f: x }\n}") + "struct에 저장할 수 없습니다") + +(* --- use의 전염 --- *) + +let () = + check "빌린 값을 capture한 클로저는 빌린 값이다" + (move_has + (res ^ "fn sink(own h: fn())\nfn f(x: F) {\n sink(fn() { peek(x) })\n}") + "use 값은 탈출하지 못합니다"); + check "빌려 쓰는 자리로는 넘길 수 있다" + (move_ok + (res ^ "fn borrow(h: fn())\nfn f(x: F) {\n borrow(fn() { peek(x) })\n}")) + +(* --- callable affinity --- *) + +let () = + check "affine 값을 capture하면 affine fn" + (move_ok (res ^ "fn f(own x: F) -> affine fn() {\n fn() { drop(x) }\n}")); + check "affine 클로저를 fn 자리에 반환하면 오류" + (move_has + (res ^ "fn f(own x: F) -> fn() {\n fn() { drop(x) }\n}") + "affine fn이어야 합니다"); + check "by-move capture는 바깥에서 소비다" + (move_has + (res + ^ "fn f(own x: F) -> affine fn() {\n\ + \ let g = fn() { drop(x) }\n\ + \ drop(x)\n\ + \ g\n\ + }") + "이미 move") + +(* --- affinity 전이 --- *) + +let () = + check "capability를 필드로 가지면 전이적으로 affine" + (move_has + (res ^ "struct B {\n f: F,\n}\nfn g(b: B) -> B {\n b\n}") + "반환할 수 없습니다"); + check "copyable 선언과 affine 필드는 공존할 수 없다" + (move_has (res ^ "copyable struct B {\n f: F,\n}") "copyable로 선언되었지만"); + check "affine이 없으면 copyable" + (move_ok "copyable struct B {\n n: Int,\n}\nfn g(b: B) -> B {\n b\n}"); + check "컨테이너를 통해서도 전이된다" + (move_has (res ^ "fn g(x: List[F]) -> List[F] {\n x\n}") "반환할 수 없습니다") + +(* --- 클로저의 mut capture 금지 --- *) + +let () = + check "클로저는 mut 바인딩을 capture할 수 없다" + (move_has + "fn sink(h: fn())\n\ + fn f() {\n\ + \ let mut n = 0\n\ + \ sink(fn() { n = n + 1 })\n\ + }" + "mut 바인딩"); + check "불변 바인딩은 capture해도 된다" + (move_ok "fn sink(h: fn())\nfn f() {\n let n = 0\n sink(fn() { n })\n}") + +(* --- 외부 타입은 affine임을 증명할 수 없다 --- *) + +let () = + check "모르는 타입은 copyable로 본다" (move_ok "fn f(x: Widget) -> Widget {\n x\n}")