1structure m0_core_decompLib :> m0_core_decompLib = 2struct 3 4open HolKernel Parse boolLib bossLib 5open m0_core_decompTheory core_decompilerLib tripleLib m0_decompLib 6 7val ERR = Feedback.mk_HOL_ERR "m0_core_decompLib" 8 9val _ = Parse.hide "cond" 10 11(* ------------------------------------------------------------------------ *) 12 13local 14 val count_INTRO_rule = 15 stateLib.introduce_triple_definition 16 (false, m0_decompTheory.m0_COUNT_def) o 17 Thm.INST [``endianness:bool`` |-> boolSyntax.F, 18 ``spsel:bool`` |-> boolSyntax.F] 19in 20 val spec = 21 List.map (count_INTRO_rule o 22 m0_progLib.memory_introduction o 23 m0_progLib.register_introduction o 24 m0_progLib.m0_introduction) o 25 m0_progLib.m0_spec 26end 27 28(* ------------------------------------------------------------------------ *) 29 30val get_cond' = 31 tripleSyntax.get_component (Lib.equal (Term.mk_var ("cond'", Type.bool))) 32 33local 34 val ARITH_SUB_CONV = 35 Conv.DEPTH_CONV bitstringLib.v2w_n2w_CONV 36 THENC wordsLib.WORD_ARITH_CONV 37 THENC wordsLib.WORD_SUB_CONV 38 fun is_reducible tm = 39 case Lib.total wordsSyntax.dest_word_add tm of 40 SOME (v, _) => not (Term.is_var v) 41 | _ => not (boolSyntax.is_cond tm) 42 fun PC_CONV tm = if is_reducible tm then ARITH_SUB_CONV tm else ALL_CONV tm 43 val WGROUND_RW_CONV = 44 Conv.DEPTH_CONV (utilsLib.cache 10 Term.compare bitstringLib.v2w_n2w_CONV) 45 THENC utilsLib.WALPHA_CONV 46 THENC utilsLib.WGROUND_CONV 47 THENC utilsLib.WALPHA_CONV 48 val cnv1 = m0_progLib.REG_CONV 49 THENC WGROUND_RW_CONV 50 THENC REWRITE_CONV [alignmentTheory.aligned_numeric] 51 val cnv2 = 52 tripleLib.CODE_CONV (Conv.DEPTH_CONV bitstringLib.v2w_n2w_CONV) 53 THENC tripleLib.POST_CONV (Conv.RAND_CONV PC_CONV) 54in 55 fun simp_triple_rule thm = 56 let 57 val thm1 = utilsLib.ALL_HYP_CONV_RULE cnv1 thm 58 val _ = get_cond' thm1 <> boolSyntax.F orelse 59 raise ERR "simp_triple_rule" "condition false" 60 in 61 Conv.CONV_RULE cnv2 thm1 62 end 63end 64 65val pc = Term.mk_var ("pc", ``:word32``) 66 67val get_code = 68 snd o pairSyntax.dest_pair o 69 hd o pred_setSyntax.strip_set o 70 tripleSyntax.dest_code o Thm.concl 71 72local 73 val get_opcode = m0_progLib.mk_thumb2_pair false o Term.rand o get_code 74 val spec_label_set = ref (Redblackset.empty String.compare) 75 val triple_rwts = ref (LVTermNet.empty: thm LVTermNet.lvtermnet) 76 fun add1 thm = 77 triple_rwts := utilsLib.add_to_rw_net get_opcode (thm, !triple_rwts) 78 val rule = tripleLib.spec_to_triple_rule (pc, M0_ASSERT_def, L3_M0_def) 79 val add_triples = List.app (add1 o rule) 80 fun find_triple opc = Lib.total (utilsLib.find_rw (!triple_rwts)) opc 81 fun spec_spec opc thm = 82 let 83 val thm_opc = get_opcode thm 84 val a = fst (Term.match_term thm_opc opc) 85 in 86 simp_triple_rule (Thm.INST a thm) 87 end 88in 89 fun addInstructionClass s = 90 if Redblackset.member (!spec_label_set, s) 91 then false 92 else (print (" " ^ s) 93 ; add_triples (spec s) 94 ; spec_label_set := Redblackset.add (!spec_label_set, s) 95 ; true) 96 fun m0_triple_hex looped s = 97 let 98 val opc = m0_stepLib.hex_to_bits s 99 in 100 case find_triple opc of 101 SOME thms => 102 let 103 val l = List.mapPartial (Lib.total (spec_spec opc)) thms 104 in 105 if List.null l 106 then loop looped opc "failed to find suitable spec" s 107 else l 108 end 109 | NONE => loop looped opc "failed to add suitable spec" s 110 end 111 and loop looped opc e s = 112 if looped orelse 113 not (addInstructionClass (m0_stepLib.thumb_instruction opc)) 114 then raise ERR "m0_triple_hex" (e ^ ": " ^ s) 115 else m0_triple_hex true s 116 val m0_triple_hex = m0_triple_hex false 117end 118 119(* ------------------------------------------------------------------------ *) 120 121local 122 val sym_abbr_thm = GSYM markerTheory.Abbrev_def 123 val swap_disj_abbr_thm = Q.prove( 124 `!x y. x \/ y = Abbrev (y \/ x)`, 125 utilsLib.qm_tac [markerTheory.Abbrev_def]) 126 val swap_conj_abbr_thm = Q.prove( 127 `!x y. x /\ y = Abbrev (y /\ x)`, 128 utilsLib.qm_tac [markerTheory.Abbrev_def]) 129in 130 fun abbrev_into_conv c = 131 case Lib.total boolSyntax.dest_disj c of 132 SOME (a, b) => 133 let 134 val d = boolSyntax.mk_disj (b, a) 135 in 136 ONCE_DEPTH_CONV 137 (fn t => if t = c 138 then Thm.SPEC c sym_abbr_thm 139 else if t = d 140 then Drule.SPECL [b, a] swap_disj_abbr_thm 141 else NO_CONV t) 142 end 143 | NONE => 144 (case Lib.total boolSyntax.dest_conj c of 145 SOME (a, b) => 146 let 147 val d = boolSyntax.mk_conj (b, a) 148 in 149 ONCE_DEPTH_CONV 150 (fn t => if t = c 151 then Thm.SPEC c sym_abbr_thm 152 else if t = d 153 then Drule.SPECL [b, a] swap_conj_abbr_thm 154 else NO_CONV t) 155 end 156 | NONE => 157 ONCE_DEPTH_CONV 158 (fn t => if t = c 159 then Thm.SPEC c sym_abbr_thm 160 else NO_CONV t)) 161end 162 163local 164 fun get_length th = if sumSyntax.is_inl (get_code th) then 2 else 4 165 val get_pc = Term.rand o Term.rand 166 fun find_exit thm = 167 let 168 val (_, p, _, q) = tripleSyntax.dest_triple (Thm.concl thm) 169 in 170 stateLib.get_delta (get_pc p) (get_pc q) 171 end 172 fun format_thm th = (th, get_length th, find_exit th) 173 val fix_precond = 174 fn [th1, th2] => 175 let 176 val c = snd (boolSyntax.dest_conj (get_cond' th2)) 177 val c = utilsLib.mk_negation c 178 in 179 [utilsLib.ALL_HYP_CONV_RULE (abbrev_into_conv c) th1, th2] 180 end 181 | thms as [_] => thms 182 | _ => raise ERR "fix_precond" "" 183 val finalise = List.map format_thm o fix_precond 184in 185 fun m0_triple hex = 186 case finalise (m0_triple_hex hex) of 187 [x] => (x, NONE) 188 | [x1, x2] => (x1, SOME x2) 189 | _ => raise ERR "m0_triple" "" 190 val m0_triple_code = 191 List.map m0_triple o 192 (m0AssemblerLib.m0_code: string quotation -> string list) 193end 194 195val vars = Term.mk_var ("cond", Type.bool) :: 196 fst (boolSyntax.strip_forall (Thm.concl M0_ASSERT_def)) 197 198fun config_for_m0 () = 199 core_decompilerLib.configure 200 { pc_tm = pc, 201 init_fn = Lib.I, 202 pc_conv = RAND_CONV, 203 triple_fn = m0_triple, 204 component_vars = vars } 205 206val () = config_for_m0 () 207 208fun m0_core_decompile name qcode = 209 ( config_for_m0 () 210 ; core_decompilerLib.code_parser := NONE 211 ; core_decompilerLib.core_decompile name qcode 212 ) 213 214fun m0_core_decompile_code name qcode = 215 ( config_for_m0 () 216 ; core_decompilerLib.code_parser := SOME (m0AssemblerLib.m0_code) 217 ; core_decompilerLib.core_decompile name qcode 218 ) 219 220(* ------------------------------------------------------------------------ *) 221 222(* Testing... 223 224open m0_core_decompLib 225 226val (test_cert, test_def) = m0_core_decompLib.m0_core_decompile "test"` 227 2100 (* movs r1, #0 *) 228 0003 (* mov r3, r0 *) 229 3328 (* adds r3, #40 *) 230 6842 (* l1: ldr r2, [r0, #4] *) 231 3004 (* adds r0, #4 *) 232 4411 (* add r1, r2 *) 233 4298 (* cmp r0, r3 *) 234 DBFA (* blt l1 *)` 235 236val (test2_cert, test2_def) = m0_core_decompLib.m0_core_decompile_code "test2" 237 `movs r1, #0 ; accumulator 238 mov r3, r0 ; first address 239 adds r3, #40 ; last address (10 loads) 240l1: ldr r2, [r0, #4] ; load data 241 adds r0, #4 ; increment address 242 add r1, r2 ; add to accumulator 243 cmp r0, r3 ; test if done 244 blt l1 ; loop if not done` 245 246val () = utilsLib.add_datatypes [``:RName``] computeLib.the_compset 247val () = computeLib.add_funs 248 [test_def, alignmentTheory.aligned_def, alignmentTheory.align_def] 249val eval = 250 EVAL THENC ONCE_DEPTH_CONV (updateLib.SORT_ENUM_UPDATES_CONV ``:RName``) 251 252eval ``test (T, (\a. if a && 3w = 0w then 4w else 0w), dmem, 253 (\x. 12w), UNIV, 0, F, F, F, F)`` 254 255val test = Count.apply m0_triple 256 257test "D000"; 258test "D100"; 259test "D200"; 260test "D300"; 261test "D400"; 262test "D500"; 263test "D600"; 264test "D700"; 265test "D800"; 266test "D900"; 267test "DA00"; 268test "DB00"; 269test "DC00"; 270test "DD00"; 271 272*) 273 274(* ------------------------------------------------------------------------ *) 275 276end 277