~thestr4ng3r/wasmcert-isabelle

53027ee3ee63c0c7fb8a1dc3434376c012e78455 — Florian Märkl 1 year, 4 months ago 862ea37
A bit more Demo
M WebAssembly/Demo/Demo.thy => WebAssembly/Demo/Demo.thy +2 -2
@@ 3,14 3,14 @@ theory Demo
begin

ML\<open>
val (module, s, i, exps, start) = load @{theory} "linear.wasm"
val (module, s, i, exps, start) = load @{theory} "block.wasm"
val state = Wasm.c_init s (Wasm.nat_of_integer 0) []
\<close>


ML\<open>
val _ = let
  val (Wasm.Set s') = Wasm.c_run  (Wasm.nat_of_integer 5) state
  val (Wasm.Set s') = Wasm.c_run  (Wasm.nat_of_integer 4) state
  val r = Wasm.show_es (Wasm.c_es (List.nth (s', 0)))
in
  writeln r

A WebAssembly/Demo/block.wasm => WebAssembly/Demo/block.wasm +0 -0
M WebAssembly/PC_Interpreter/Interpreter.thy => WebAssembly/PC_Interpreter/Interpreter.thy +1 -1
@@ 460,7 460,7 @@ definition c_init :: "s \<Rightarrow> nat \<Rightarrow> v list \<Rightarrow> c_s
  "c_init s fi args \<equiv> \<lparr>
    c_s = s,
    c_pc = \<lparr> c_fi = fi, c_ei = 0, c_d = D_None \<rparr>,
    c_locs = args, \<comment>\<open>TODO: init non-arg locals\<close>
    c_locs = args @ (case s.funcs s ! fi of Func_native _ _ lt _  \<Rightarrow> n_zeros lt),
    val_stack = [],
    call_stack = [],
    trapped = False,

M WebAssembly/SML/Wasm_Show.thy => WebAssembly/SML/Wasm_Show.thy +24 -6
@@ 37,15 37,33 @@ local_setup \<open>
  #> Show_Generator.register_foreign_showsp @{typ f64} @{term "showsp_f64"} @{thm show_law_f64}
\<close>

derive "show" i32 i64 f32 f64 unop_i unop_f unop sx binop_i binop_f binop
  testop relop_i relop_f relop cvtop v tp t tf
derive "show" i32 i64 f32 f64 t

definition showsp_tf :: "tf showsp" where
  "showsp_tf p tf \<equiv> case tf of (at _> rt) \<Rightarrow>
    shows_pl p o shows at o shows_string '' _> '' o shows rt o shows_pr p"

lemma show_law_tf [show_law_intros]:
  "show_law showsp_tf r"
  by (rule show_lawI) (simp add: showsp_tf_def show_law_simps split: tf.splits)

local_setup \<open>
  Show_Generator.register_foreign_showsp @{typ tf} @{term "showsp_tf"} @{thm show_law_tf}
\<close>

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 _ (Block tf bbs) = shows_string ''Block''" |
  "showsp_b_e 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 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''" |


@@ 64,15 82,15 @@ fun showsp_b_e :: "b_e showsp" where
  "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 _ (Unop t unop) = shows_string ''Unop''" |
  "showsp_b_e _ (Binop t binop) = shows_string ''Binop''" |
  "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) (cases r, auto simp: show_law_simps)
  by (rule show_lawI) (induction r, auto simp: show_law_simps)

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