Module DebugAbMemCsharpminor

Require Import
  Utf8 String ToString Util
  DebugLib DebugCshm
  TypesDomain
  AbMemSignatureCsharpminor.

Set Implicit Arguments.

Local Open Scope string_scope.

Section S.

  Context t t_iter `(MD:mem_dom t t_iter) `{ToString t} `{ToString t_iter}
          (verbose: bool).

  Instance debug_mem_dom : mem_dom t t_iter :=
    { widen_mem := widen_print
    ; assign x e ab :=
        let r := assign x e ab in
        let s := to_string x ++ " ← " ++ to_string e
              ++ if verbose then " ⇒ " ++ to_string (fst r) else "" in
        print s r
    ; assign_any x ty ab :=
        let r := assign_any x ty ab in
        let s := to_string x ++ " ← any " ++ to_string ty
              ++ if verbose then " ⇒ " ++ to_string (fst r) else "" in
        print s r
    ; store κ a e ab :=
        let r := store κ a e ab in
        let s := to_string κ ++ "[" ++ to_string a ++ "] := " ++ to_string e
              ++ if verbose then " ⇒ " ++ to_string (fst r) else "" in
        print s r
    ; assume e ab :=
        let r := assume e ab in
        let s := "assume " ++ to_string e in
        print s r
    ; noerror e ab :=
        let r := noerror e ab in
        let s := "noerror " ++ to_string e in
        print s r
    ; ab_vload r gofs args ab :=
        let r := ab_vload r gofs args ab in
        let s := "ab_vload " ++ " " ++ match gofs with Some (g, ofs) => string_of_ident g ++ " " ++ PrintPos.string_of_z (Integers.Int.unsigned ofs) | None => "" end ++ to_string args in
        print s r
    ; ab_vstore r gofs args ab :=
        let r := ab_vstore r gofs args ab in
        let s := "ab_vstore " ++ " " ++ match gofs with Some (g, ofs) => string_of_ident g ++ " " ++ PrintPos.string_of_z (Integers.Int.unsigned ofs) | None => "" end ++ to_string args in
        print s r
    ; deref_fun e ab :=
        let r := deref_fun e ab in
        let s := "deref_fun " ++ to_string e in
        print s r
    ; push_frame f args ab :=
        let r := push_frame f args ab in
        let s := "push_frame "
              ++ if verbose then " ⇒ " ++ to_string (fst r) else "" in
        print s r
    ; pop_frame ret rettemp ab :=
        let r := pop_frame ret rettemp ab in
        let s := "pop_frame"
              ++ if verbose then " ⇒ " ++ to_string (fst r) else "" in
        print s r
    ; ab_malloc e x ab :=
        let r := ab_malloc e x ab in
        let s := "ab_malloc" in
        print s r
    ; ab_free e ab :=
        let r := ab_free e ab in
        let s := "ab_free" in
        print s r
    ; ab_memcpy sz al dst src ab :=
        let r := ab_memcpy sz al dst src ab in
        let s := "ab_memcpy(" ++ to_string sz ++ ", " ++ to_string al ++ ", " ++ to_string dst ++ ", " ++ to_string src ++ ")" in
        print s r
    ; init_mem defs :=
        let r := init_mem defs in
        let s := "init_mem" ++ if verbose then " ⇒ " ++ to_string (fst r) else "" in
        print s r
    }.

  Lemma debug_mem_dom_sound:
    ∀ ge gamma gamma_iter,
      mem_dom_spec ge MD gamma gamma_iter ->
      mem_dom_spec ge debug_mem_dom gamma gamma_iter.

End S.