1open HolKernel Parse boolLib bossLib; 2open m0_decompLib 3 4val () = new_theory "m0_decomp_demo"; 5 6(* test program *) 7val q = 8 `movs r1, #0 ; accumulator 9 mov r3, r0 ; first address 10 adds r3, #40 ; last address (10 loads) 11l1: ldr r2, [r0, #4] ; load data 12 adds r0, #4 ; increment address 13 add r1, r2 ; add to accumulator 14 cmp r0, r3 ; test if done 15 blt l1 ; loop if not done` 16 17(* from GAS *) 18val (test_cert, test_def) = m0_decompile "test" ` 19 2100 20 0003 21 3328 22 6842 23 3004 24 4411 25 4298 26 DBFA` 27 28(* internal assembler *) 29val () = m0AssemblerLib.print_m0_code q 30 31val (test2_cert, test2_def) = m0_decompile_code "test2" q 32 33val () = computeLib.add_funs [test_def] 34val () = computeLib.add_funs [test2_def] 35 36val run1 = Theory.save_thm("run1", 37 EVAL ``test (12w, 0, dmem, \a. if a && 3w = 0w then 4w else 0w)``) 38 39val run2 = Theory.save_thm("run2", 40 EVAL ``test2 (12w, 0, dmem, \a. if a && 3w = 0w then 4w else 0w)``) 41 42val () = export_theory() 43