1open HolKernel Parse boolLib bossLib;
2open riscv_decompLib
3
4val () = new_theory "riscv_decomp_demo";
5
6val () = utilsLib.add_to_the_compset ([], riscvTheory.inventory)
7
8local
9  fun assemble1 tm =
10     stringSyntax.fromHOLstring
11       (utilsLib.rhsc (EVAL ``word_to_hex_string (riscv$Encode ^tm)``))
12in
13  val assemble = utilsLib.strings_to_quote o List.map assemble1
14end
15
16fun riscv_decompile_code s = riscv_decompLib.riscv_decompile s o assemble
17
18val (text1_cert, test1_def) = riscv_decompile_code "test1"
19  [
20   ``ArithI (ADDI (1w, 2w, 4w))``,
21   ``MulDiv (MUL (1w, 3w, 1w))``,
22   ``ArithR (ADD (2w, 1w, 1w))``
23  ]
24
25val (text2_cert, test2_def) = riscv_decompile_code "test2"
26  [
27   ``ArithI (ADDI (1w, 1w, -1w))``,
28   ``Branch (BEQ (1w, 0w, -2w))``
29  ]
30
31val () = computeLib.add_funs [test1_def, test2_def]
32
33val run1 = Theory.save_thm ("run1",
34  EVAL ``test1 (20w, 11w)``
35  )
36
37val run2 = Theory.save_thm ("run2",
38  EVAL ``test2 11w``
39  )
40
41val () = export_theory()
42