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