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