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