1structure m0_decompLib :> m0_decompLib =
2struct
3
4open HolKernel Parse boolLib bossLib
5open decompilerLib m0_progLib m0_progTheory m0_decompTheory
6
7val () = m0_progLib.set_newline ""
8
9val ERR = mk_HOL_ERR "m0_decompLib"
10
11local
12   fun get_length th =
13      if sumSyntax.is_inl (m0_progLib.get_code th) then 2 else 4
14   val find_exit =
15      stateLib.get_pc_delta
16          (Lib.equal "m0_prog$m0_PC" o fst o boolSyntax.dest_strip_comb)
17   fun format_thm th = (th, get_length th, find_exit th)
18   val count_INTRO_rule =
19      stateLib.introduce_triple_definition (false, m0_COUNT_def) o
20      Thm.INST [``endianness:bool`` |-> boolSyntax.F,
21                ``spsel:bool`` |-> boolSyntax.F]
22   val finalise =
23      List.map format_thm o stateLib.fix_precond o List.map count_INTRO_rule
24in
25   val set_opt = m0_progLib.m0_config false
26   fun m0_triples hex =
27      case finalise (m0_progLib.m0_spec_hex hex) of
28         [x] => (x, NONE)
29       | [x1, x2] => (x1, SOME x2)
30       | _ => raise ERR "m0_triples" ""
31   fun m0_triples_opt s hex = (set_opt s; m0_triples hex)
32end
33
34val m0_pc = Term.prim_mk_const {Thy = "m0_prog", Name = "m0_PC"}
35
36fun m0_tools f hide = (f, fn _ => fail(), hide, m0_pc): decompiler_tools
37fun m0_tools_opt opt = m0_tools (m0_triples_opt opt)
38
39val l3_m0_tools = m0_tools m0_triples m0_NZCV_HIDE
40val l3_m0_tools_no_status = m0_tools m0_triples TRUTH
41
42val l3_m0_tools_flat = m0_tools_opt "flat" m0_NZCV_HIDE
43val l3_m0_tools_array = m0_tools_opt "array" m0_NZCV_HIDE
44val l3_m0_tools_mapped = m0_tools_opt "mapped" m0_NZCV_HIDE
45
46val l3_m0_tools_flat_no_status = m0_tools_opt "flat" TRUTH
47val l3_m0_tools_array_no_status = m0_tools_opt "array" TRUTH
48val l3_m0_tools_mapped_no_status = m0_tools_opt "mapped" TRUTH
49
50fun m0_decompile name qcode =
51   (set_opt "mapped"; decompilerLib.decompile l3_m0_tools name qcode)
52
53fun m0_decompile_code name (qass: string quotation) =
54   ( set_opt "mapped"
55   ; decompilerLib.decompile_with m0AssemblerLib.m0_code l3_m0_tools name qass
56   )
57
58end
59