Lec12.Semantic Analysis (3) - 13주차 1강

11월 25일 13주차 1강

* 개인 공부를 위해 정리한 것입니다. 정확한 내용은 꼭 본인이 공부하는 교재를 참고하시기 바랍니다.

대충 Lec 11에서 계속 배우던 연산, 불리안, 코맨드 구현의 코드를 깃허브에 올려놓으셨단 뜻

아래 렉쳐 슬라이드에서는 코드 중 일부를 가져와서 설명함

 

module Sign = struct
  type t = Top | Bot | Pos | Neg | Zero | NonPos | NonNeg | NonZero
  let porder : t -> t -> bool
  = fun s1 s2 ->
  match s1, s2 with
  | _, _ when s1 = s2 -> true  (* 동일한 값은 포함 관계 성립 *)
  | Bot, _ -> true             (* NONE은 모든 값의 부분집합. 어떤 값도 포함하지 않음 *)
  | _, Top -> true             (* 모든 값은 ANY의 부분집합 *)
  | Neg, NonPos -> true        (* 음수는 Non-Pos의 부분집합 *)
  | Neg, NonZero -> true       (* 음수는 Non-Zero의 부분집합 *)
  | Zero, NonPos -> true       (* 0은 Non-Pos의 부분집합 *)
  | ...                        (* 나머지 조건들 추가 *)

module AbsBool = struct
  type t = Top | Bot | True | False

  let porder : t -> t -> bool
  = fun b1 b2 ->
  if b1 = b2 then true (* 두 값이 같으면 true *)
  else
    match b1,b2 with 
    | Bot,_ -> true (* None은 모든 값의 부분집합 *)
    | _,Top -> true (* 모든 값은 Any의 부분집합 *)
    | _,_ -> false (* 나머지 경우는 부분 순서를 만족하지 않음 *)
end

 

• 변수 집합 Var에서 Sign으로 매핑됨
• 부분 순서: s1과 s2의 관계는 모든 변수 x에 대해 각 기호의 부분 순서 관계를 만족해야 함

module AbsMem = struct
  (* Map 모듈을 String 키를 사용해 초기화. 
     변수 이름(String)이 키가 되고, 값은 Sign.t 타입이 됨 *)
  module Map = Map.Make(String) 

  (* 추상 메모리 상태의 타입 정의:
     변수(Var)를 키로, 기호(Sign.t)를 값으로 가지는 맵 구조. *)
  type t = Sign.t Map.t 

  (* 부분 순서 함수 정의:
     두 추상 상태(m1, m2) 사이의 포함 관계를 결정. *)
  let porder : t -> t -> bool
  = fun m1 m2 ->
    (* m1의 모든 키-값 쌍이 조건을 만족하는지 확인. *)
    Map.for_all
      (fun x v -> 
        (* m1에서 키 x의 값 v와 m2에서 동일한 키 x의 값을 비교. *)
        Sign.porder v (Map.find x m2))
      m1
end

 

• m1​={x→Pos,y→Zero}, m2={x→NonNeg,y→NonPos}
• Pos⊑NonNeg, Zero⊑NonPos이므로 m1​⊑m2​. (각 x,y에 대해 포함관계가 성립)

 

let rec eval_a : aexp -> AbsMem.t -> Sign.t
= fun a m ->
  match a with
  | Int n -> Sign.alpha n           (* 상수 값은 Sign.alpha를 통해 기호 값으로 변환 *)
  | Var x -> AbsMem.find x m        (* 변수 값은 메모리 상태 m에서 검색 *)
  | Plus (a1, a2) ->                (* 덧셈 *)
      Sign.add (eval_a a1 m) (eval_a a2 m)
      
 module Sign = struct
  let add : t -> t -> t
  = fun s1 s2 ->
    match s1, s2 with
    | Bot, _ | _, Bot -> Bot          (* NONE과의 연산 결과는 NONE *)
    | _, Top | Top, _ -> Top          (* ANY와의 연산 결과는 ANY *)
    | Neg, Neg -> Neg                 (* 음수 + 음수 = 음수 *)
    | Neg, Zero -> Neg                (* 음수 + 0 = 음수 *)
    | Neg, NonPos -> Neg              (* 음수 + (0 또는 음수) = 음수 *)
    | ...                             (* 다른 경우는 추가 정의 필요 *)

 

let rec eval_b : bexp -> AbsMem.t -> AbsBool.t
= fun b m ->
  match b with
  | True -> AbsBool.True                       (* 참 표현식은 True 반환 *)
  | False -> AbsBool.False                     (* 거짓 표현식은 False 반환 *)
  | Eq (a1, a2) ->                             (* a1 = a2 평가 *)
      Sign.eq (eval_a a1 m) (eval_a a2 m)
  | Leq (a1, a2) ->                            (* a1 <= a2 평가 *)
      Sign.leq (eval_a a1 m) (eval_a a2 m)
  | Not b -> AbsBool.not (eval_b b m)          (* 부울 표현식의 부정 *)
  | And (b1, b2) ->                            (* 논리곱 *)
      AbsBool.band (eval_b b1 m) (eval_b b2 m)

module Sign = struct
  let eq = ...        (* 추상 값의 동등성 비교 *)
  let leq = ...       (* 추상 값의 크기 비교 *)
end

module AbsBool = struct
  let not = ...       (* 부울 값의 부정 *)
  let band = ...      (* 부울 값의 논리곱 *)
end

• 명령문 c가 주어진 state를 받아 새로운 state로 반환
• 대입문, 변수 x에 표현식 a를 평가한 결과를 할당. 상태 s는 변수 x의 값을 a의 평가 결과로 업데이트
• skip, 상태를 변경하지 않음
• 명령문 연결, c1을 실행한 후 c2를 실행
• if문, 조건 b를 평가한 결과에 따라 참이면 c1, 거짓이면 c2 실행
• while문, 조건 b가 참인 동안 c를 반복 실행, 고정점을 계산해 반복적으로 상태 병합

 

let rec eval_c : cmd -> AbsMem.t -> AbsMem.t
= fun c m ->
  match c with
  (* 변수 할당 *)
  | Assign (x, a) -> AbsMem.add x (eval_a a m) m
  (* Skip: 상태를 그대로 유지 *)
  | Skip -> m
  (* 두 명령문의 순차 실행 *)
  | Seq (c1, c2) -> eval_c c2 (eval_c c1 m)
  (* 조건문 *)
  | If (b, c1, c2) -> cond (eval_b b, eval_c c1, eval_c c2) m
  (* While-loop *)
  | While (b, c) ->
      let onestep x = AbsMem.join m (eval_c c x) in
      let rec fix f x i =
        let x' = f x in
        if AbsMem.porder x' x then x (* 안정된 상태에 도달 *)
        else fix f x' (i+1) (* 안정되지 않았다면 재귀적으로 반복 *)
      in
      fix onestep m 1