71 open Hints_declaration
91 (** val jump_expansion_internal :
92 ASM.labelled_instruction List.list Types.sig0 -> Nat.nat -> (Bool.bool,
93 PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **)
94 let rec jump_expansion_internal program n =
95 let labels = PolicyFront.create_label_map (Types.pi1 program) in
97 prerr_endline "JEI_start";
98 let { Types.fst = no_ch; Types.snd = z } = res in
101 { Types.fst = Bool.False; Types.snd = Types.None }
108 (PolicyStep.jump_expansion_step program (Types.pi1 labels)
112 { Types.fst = Bool.False; Types.snd =
114 (PolicyFront.jump_expansion_start program (Types.pi1 labels))) }
118 (fun _ -> { Types.fst = Bool.False; Types.snd =
120 (PolicyFront.jump_expansion_start program (Types.pi1 labels))) })
123 let res = Types.pi1 (jump_expansion_internal program m) in
124 (let { Types.fst = no_ch; Types.snd = z } = res in
128 (fun _ -> { Types.fst = Bool.False; Types.snd = Types.None })
135 (PolicyStep.jump_expansion_step program (Types.pi1 labels)
138 (** val measure_int :
139 ASM.labelled_instruction List.list -> PolicyFront.ppc_pc_map -> Nat.nat
141 let rec measure_int program policy acc =
144 | List.Cons (h, t) ->
145 (match (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
146 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
147 (Nat.S Nat.O))))))))))))))))
148 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
149 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
150 (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length t))
151 policy.Types.snd { Types.fst = Nat.O; Types.snd =
152 Assembly.Short_jump }).Types.snd with
153 | Assembly.Short_jump -> measure_int t policy acc
154 | Assembly.Absolute_jump ->
155 measure_int t policy (Nat.plus acc (Nat.S Nat.O))
156 | Assembly.Long_jump ->
157 measure_int t policy (Nat.plus acc (Nat.S (Nat.S Nat.O))))
159 (** val je_fixpoint :
160 ASM.labelled_instruction List.list Types.sig0 -> PolicyFront.ppc_pc_map
161 Types.option Types.sig0 **)
162 let je_fixpoint program =
164 (jump_expansion_internal program (Nat.S
165 (Nat.times (Nat.S (Nat.S Nat.O)) (List.length (Types.pi1 program)))))).Types.snd
167 (** val jump_expansion' :
168 ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word,
169 BitVector.word -> Bool.bool) Types.prod Types.sig0 Types.option **)
170 let jump_expansion' program =
171 let program' = program.ASM.code in
172 let f = Types.pi1 (je_fixpoint program') in
174 | Types.None -> (fun _ -> Types.None)
176 (fun _ -> Types.Some { Types.fst = (fun ppc ->
178 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
179 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
180 (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
181 Types.snd = Assembly.Short_jump }).Types.fst
183 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
184 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
185 (Nat.S Nat.O)))))))))))))))) pc); Types.snd = (fun ppc ->
187 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
188 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
189 (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
190 Types.snd = Assembly.Short_jump }).Types.snd
192 PolicyFront.jmpeqb jl Assembly.Long_jump) })) __