~thestr4ng3r/wasmcert-isabelle

22f8f8ca69390a0df9f1219f7e7f10a7517b9ca8 — Florian Märkl 1 year, 4 months ago 2d8d14b master
Add Pretty Printing
M WebAssembly/Demo/Demo.thy => WebAssembly/Demo/Demo.thy +2 -2
@@ 18,7 18,7 @@ fun run_and_show state fuel =
      in
        writeln ("  program counter: " ^ (Int.toString (Wasm.integer_of_nat (Wasm.c_ei (Wasm.c_pc s')))));
        writeln ("  value stack:     " ^ (Wasm.show_vs (Wasm.val_stack s')));
        writeln ("  reconstruction:  " ^ Wasm.show_es (Wasm.c_es s'));
        writeln ("  reconstruction:\n    " ^ Wasm.show_es_pretty (Wasm.nat_of_integer 2) (Wasm.c_es s'));
        if Wasm.terminated s' then writeln "  TERMINATED! ==================================" else ()
      end
    else


@@ 30,7 30,7 @@ fun show_function s i =
    val es = case List.nth (Wasm.funcs s, i) of
      Wasm.Func_native (_, _, _, es) => es
      | _ => raise (Fail "not a native function")
    val r = Wasm.show_b_es es
    val r = Wasm.show_b_es_pretty (Wasm.nat_of_integer 0) es
  in
    writeln r
  end

M WebAssembly/SML/Printing.thy => WebAssembly/SML/Printing.thy +2 -0
@@ 272,7 272,9 @@ instance apply standard unfolding equal_mem_rep_def .. end

definition show_es :: "e list \<Rightarrow> String.literal" where "show_es es \<equiv> String.implode (show es)"
definition show_b_es :: "b_e list \<Rightarrow> String.literal" where "show_b_es bs \<equiv> String.implode (show bs)"
definition show_b_es_pretty :: "nat \<Rightarrow> b_e list \<Rightarrow> String.literal" where "show_b_es_pretty indent bs \<equiv> String.implode (shows_b_es_pretty indent bs '''')"
definition show_vs :: "v list \<Rightarrow> String.literal" where "show_vs vs \<equiv> String.implode (show vs)"
definition show_es_pretty :: "nat \<Rightarrow> e list \<Rightarrow> String.literal" where "show_es_pretty indent es \<equiv> String.implode (shows_es_pretty indent es '''')"

export_code open m_imports module_type_checker interp_instantiate typing run c_run
  in SML module_name WasmRef_Isa file_prefix WasmRef_Isa

M WebAssembly/SML/Reflect.thy => WebAssembly/SML/Reflect.thy +1 -1
@@ 16,7 16,7 @@ code_reflect Wasm
    and s_ext = _
  functions m_imports module_type_checker interp_instantiate typing run c_run
    nat_of_integer integer_of_nat SML_int32_to_isabelle_int32 SML_int64_to_isabelle_int64 SML_char_to_isabelle_byte
    c_init c_step c_run c_es s.funcs show_es show_b_es Func_native set terminated val_stack c_ei c_pc show_vs
    c_init c_step c_run c_es s.funcs show_es show_es_pretty show_b_es show_b_es_pretty Func_native set terminated val_stack c_ei c_pc show_vs

ML_file "Decode.ML"


M WebAssembly/SML/Wasm_Show.thy => WebAssembly/SML/Wasm_Show.thy +111 -53
@@ 54,46 54,87 @@ local_setup \<open>
derive "show" unop_i unop_f unop sx binop_i binop_f binop
  testop relop_i relop_f relop cvtop v tp tf

fun showsp_b_e :: "b_e showsp" where
  "showsp_b_e _ (Unreachable) = shows_string ''Unreachable''" |
  "showsp_b_e _ (Nop) = shows_string ''Nop''" |
  "showsp_b_e _ (Drop) = shows_string ''Drop''" |
  "showsp_b_e _ (Select) = shows_string ''Select''" |
  "showsp_b_e p (Block tf bbs) = shows_pl p o shows_string ''Block ''
definition nl_indent :: "nat \<Rightarrow> string" where
  "nl_indent indent \<equiv> ''\<newline>'' @ replicate (indent * 2) (CHR '' '')"

definition pshowsp_list_pretty :: "nat \<Rightarrow> nat \<Rightarrow> shows list \<Rightarrow> shows"
where
  "pshowsp_list_pretty indent p xs = shows_list_gen id ''[]'' (''['' @ nl_indent (Suc indent)) ('','' @ nl_indent (Suc indent) @ '''') (nl_indent indent @ '']'') xs"

definition showsp_list_pretty :: "'a showsp \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> shows"
where
  [code del]: "showsp_list_pretty s indent p = pshowsp_list_pretty indent p o map (s 0)"

lemma showsp_list_pretty_code [code]:
  "showsp_list_pretty s indent p xs = shows_list_gen (s 0) ''[]'' (''['' @ nl_indent (Suc indent)) ('','' @ nl_indent (Suc indent) @ '''') (nl_indent indent @ '']'') xs"
  by (simp add: showsp_list_pretty_def pshowsp_list_pretty_def shows_list_gen_map)

lemma show_law_list_pretty [show_law_intros]:
  "(\<And>x. x \<in> set xs \<Longrightarrow> show_law s x) \<Longrightarrow> show_law (showsp_list_pretty s indent) xs"
  by (simp add: show_law_def showsp_list_pretty_code show_law_simps)

lemma showsp_list_pretty_cong [fundef_cong]:
  "xs = ys \<Longrightarrow> p = q \<Longrightarrow>
    (\<And>p x. x \<in> set ys \<Longrightarrow> f p x = g p x) \<Longrightarrow> showsp_list_pretty f indent p xs = showsp_list_pretty g indent q ys"
  by (simp add: showsp_list_pretty_code cong: shows_list_gen_cong)

definition showsp_list_pretty_or_not :: "bool \<Rightarrow> 'a showsp \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> shows" where
  "showsp_list_pretty_or_not pretty s indent \<equiv>
    if pretty then showsp_list_pretty s indent
    else showsp_list s"

lemma showsp_list_pretty_or_not_cong [fundef_cong]:
  "xs = ys \<Longrightarrow> p = q \<Longrightarrow>
    (\<And>p x. x \<in> set ys \<Longrightarrow> f p x = g p x) \<Longrightarrow> showsp_list_pretty_or_not pretty f indent p xs = showsp_list_pretty_or_not pretty g indent q ys"
  by (simp add: showsp_list_pretty_or_not_def showsp_list_code showsp_list_pretty_code cong: shows_list_gen_cong)

fun showsp_b_e :: "bool \<Rightarrow> nat \<Rightarrow> b_e showsp" where
  "showsp_b_e _ _ _ (Unreachable) = shows_string ''Unreachable''" |
  "showsp_b_e _ _ _ (Nop) = shows_string ''Nop''" |
  "showsp_b_e _ _ _ (Drop) = shows_string ''Drop''" |
  "showsp_b_e _ _ _ (Select) = shows_string ''Select''" |
  "showsp_b_e pretty indent p (Block tf bbs) = shows_pl p o shows_string ''Block ''
      o shows_prec 1 tf
      o shows_space
      o showsp_list showsp_b_e 1 bbs
      o showsp_list_pretty_or_not pretty (showsp_b_e pretty (Suc indent)) (Suc indent) 1 bbs
    o shows_pr p" |
  "showsp_b_e _ (Loop tf bbs) = shows_string ''Loop''" |
  "showsp_b_e _ (If tf tbs fbs) = shows_string ''If''" |
  "showsp_b_e _ (Br i) = shows_string ''Br''" |
  "showsp_b_e _ (Br_if i) = shows_string ''Br_if''" |
  "showsp_b_e _ (Br_table il i) = shows_string ''Br_table''" |
  "showsp_b_e _ (Return) = shows_string ''Return''" |
  "showsp_b_e _ (Call i) = shows_string ''Call''" |
  "showsp_b_e _ (Call_indirect i) = shows_string ''Call_indirect''" |
  "showsp_b_e _ (Get_local i) = shows_string ''Get_local''" |
  "showsp_b_e _ (Set_local i) = shows_string ''Set_local''" |
  "showsp_b_e _ (Tee_local i) = shows_string ''Tee_local''" |
  "showsp_b_e _ (Get_global i) = shows_string ''Get_global''" |
  "showsp_b_e _ (Set_global i) = shows_string ''Set_global''" |
  "showsp_b_e _ (Load t al a off) = shows_string ''Load''" |
  "showsp_b_e _ (Store t al a off) = shows_string ''Store''" |
  "showsp_b_e _ (Current_memory) = shows_string ''Current_memory''" |
  "showsp_b_e _ (Grow_memory) = shows_string ''Grow_memory''" |
  "showsp_b_e p (EConst v) = shows_string ''C '' o shows_prec 1 v" |
  "showsp_b_e p (Unop t unop) = shows_pl p o shows_string ''Unop '' o shows_prec 1 t o shows_space o shows_prec 1 unop o shows_pl p" |
  "showsp_b_e p (Binop t binop) = shows_pl p o shows_string ''Unop '' o shows_prec 1 t o shows_space o shows_prec 1 binop o shows_pl p" |
  "showsp_b_e _ (Testop t testop) = shows_string ''Testop''" |
  "showsp_b_e _ (Relop t relop) = shows_string ''Relop''" |
  "showsp_b_e _ (Cvtop t2 cvtop t1 sx) = shows_string ''Cvtop''"
  "showsp_b_e _ _ _ (Loop tf bbs) = shows_string ''Loop''" |
  "showsp_b_e _ _ _ (If tf tbs fbs) = shows_string ''If''" |
  "showsp_b_e _ _ _ (Br i) = shows_string ''Br''" |
  "showsp_b_e _ _ _ (Br_if i) = shows_string ''Br_if''" |
  "showsp_b_e _ _ _ (Br_table il i) = shows_string ''Br_table''" |
  "showsp_b_e _ _ _ (Return) = shows_string ''Return''" |
  "showsp_b_e _ _ _ (Call i) = shows_string ''Call''" |
  "showsp_b_e _ _ _ (Call_indirect i) = shows_string ''Call_indirect''" |
  "showsp_b_e _ _ _ (Get_local i) = shows_string ''Get_local''" |
  "showsp_b_e _ _ _ (Set_local i) = shows_string ''Set_local''" |
  "showsp_b_e _ _ _ (Tee_local i) = shows_string ''Tee_local''" |
  "showsp_b_e _ _ _ (Get_global i) = shows_string ''Get_global''" |
  "showsp_b_e _ _ _ (Set_global i) = shows_string ''Set_global''" |
  "showsp_b_e _ _ _ (Load t al a off) = shows_string ''Load''" |
  "showsp_b_e _ _ _ (Store t al a off) = shows_string ''Store''" |
  "showsp_b_e _ _ _ (Current_memory) = shows_string ''Current_memory''" |
  "showsp_b_e _ _ _ (Grow_memory) = shows_string ''Grow_memory''" |
  "showsp_b_e _ _ p (EConst v) = shows_string ''C '' o shows_prec 1 v" |
  "showsp_b_e _ _ p (Unop t unop) = shows_pl p o shows_string ''Unop '' o shows_prec 1 t o shows_space o shows_prec 1 unop o shows_pl p" |
  "showsp_b_e _ _ p (Binop t binop) = shows_pl p o shows_string ''Unop '' o shows_prec 1 t o shows_space o shows_prec 1 binop o shows_pl p" |
  "showsp_b_e _ _ _ (Testop t testop) = shows_string ''Testop''" |
  "showsp_b_e _ _ _ (Relop t relop) = shows_string ''Relop''" |
  "showsp_b_e _ _ _ (Cvtop t2 cvtop t1 sx) = shows_string ''Cvtop''"

lemma show_law_b_e [show_law_intros]:
  "show_law showsp_b_e r"
  by (rule show_lawI) (induction r, auto simp: show_law_simps)
  "show_law (showsp_b_e pretty indent) r"
  by (rule show_lawI) (induction r arbitrary: pretty indent, auto simp: show_law_simps  showsp_list_code showsp_list_pretty_code showsp_list_pretty_or_not_def)

definition showsp_b_e_def :: "b_e showsp" where
  "showsp_b_e_def = showsp_b_e False 0"

lemma show_law_b_e_def [show_law_intros]:
  "show_law showsp_b_e_def r"
  unfolding showsp_b_e_def_def by (rule show_law_b_e)

local_setup \<open>
  Show_Generator.register_foreign_showsp @{typ b_e} @{term "showsp_b_e"} @{thm show_law_b_e}
  Show_Generator.register_foreign_showsp @{typ b_e} @{term "showsp_b_e_def"} @{thm show_law_b_e_def}
\<close>

derive "show" b_e


@@ 108,11 149,6 @@ definition showsp_f_ext :: "'a showsp \<Rightarrow> ('a f_ext) showsp"
where
  [code del]: "showsp_f_ext s1 p = pshowsp_f_ext p o map_f_ext (s1 1)"

lemma showsp_prod_simps [simp, code]:
  "showsp_prod s1 s2 p (x, y) =
    shows_string ''('' o s1 1 x o shows_string '', '' o s2 1 y o shows_string '')''"
  by (simp add: showsp_prod_def)

lemma show_law_f_ext [show_law_intros]:
  "show_law s1 (more x) \<Longrightarrow>
    show_law (showsp_f_ext s1) y"


@@ 128,28 164,50 @@ local_setup \<open>

derive "show" f_ext

fun showsp_e :: "e showsp" where
  "showsp_e p (Basic b) = shows_pl p o shows (CHR ''$'') o shows_prec 0 b o shows_pr p" |
  "showsp_e _ Trap = shows_string ''Trap''" |
  "showsp_e p (Invoke i) = shows_pl p o shows_string ''Invoke '' o shows i o shows_pr p" |
  "showsp_e p (Label n les es) =
fun showsp_e :: "bool \<Rightarrow> nat \<Rightarrow> e showsp" where
  "showsp_e pretty indent p (Basic b) = shows_pl p o shows (CHR ''$'') o showsp_b_e pretty indent 0 b o shows_pr p" |
  "showsp_e _ _ _ Trap = shows_string ''Trap''" |
  "showsp_e _ _ p (Invoke i) = shows_pl p o shows_string ''Invoke '' o shows i o shows_pr p" |
  "showsp_e pretty indent p (Label n les es) =
    shows_pl p o shows_string ''Label ''
      o shows_prec 1 n o shows_space
      o showsp_list showsp_e 1 les o shows_space
      o showsp_list showsp_e 1 es
      o shows_prec 1 n
      o shows_space
      o showsp_list (showsp_e False 0) 1 les
      o shows_space
      o showsp_list_pretty_or_not pretty (showsp_e pretty (Suc indent)) (Suc indent) 1 es
    o shows_pr p" |
  "showsp_e p (Frame n f es) = shows_pl p o shows_string ''Frame '' o shows_prec 1 n o shows_space o showsp_list showsp_e 1 es o shows_pr p"

lemma show_law_e [show_law_intros]:
  "show_law showsp_e r"
  "showsp_e pretty indent p (Frame n f es) =
    shows_pl p o
    shows_string ''Frame '' o
    shows_prec 1 n o
    shows_space o
    showsp_list_pretty_or_not pretty (showsp_e pretty (Suc indent)) (Suc indent) 1 es o
    shows_pr p"

lemma show_law_e:
  "show_law (showsp_e pretty indent) r"
  apply (rule show_lawI)
  apply (induction r)
  by (auto simp add: show_law_simps)
  apply (induction r arbitrary: pretty indent)
  apply (auto simp add: show_law_simps showsp_list_code showsp_list_pretty_code showsp_list_pretty_or_not_def)
  by (simp add: show_lawD show_law_b_e show_law_char shows_pl_append) (* this is bad *)

definition showsp_e_def :: "e showsp" where
  "showsp_e_def = showsp_e False 0"

lemma show_law_e_def [show_law_intros]:
  "show_law showsp_e_def r"
  unfolding showsp_e_def_def by (rule show_law_e)

local_setup \<open>
  Show_Generator.register_foreign_showsp @{typ e} @{term "showsp_e"} @{thm show_law_e}
  Show_Generator.register_foreign_showsp @{typ e} @{term "showsp_e_def"} @{thm show_law_e_def}
\<close>

derive "show" e

definition shows_b_es_pretty :: "nat \<Rightarrow> b_e list \<Rightarrow> string \<Rightarrow> string" where
  "shows_b_es_pretty indent es \<equiv> showsp_list_pretty (showsp_b_e True indent) indent 0 es"

definition shows_es_pretty :: "nat \<Rightarrow> e list \<Rightarrow> string \<Rightarrow> string" where
  "shows_es_pretty indent es \<equiv> showsp_list_pretty (showsp_e True indent) indent 0 es"

end