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
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 let init =(PolicyFront.jump_expansion_start program (Types.pi1 labels)) in
114 { Types.fst = Bool.False; Types.snd =
119 (fun _ -> { Types.fst = Bool.False; Types.snd =
121 (PolicyFront.jump_expansion_start program (Types.pi1 labels))) })
124 let res = Types.pi1 (jump_expansion_internal program m) in
125 (let { Types.fst = no_ch; Types.snd = z } = res in
129 (fun _ -> { Types.fst = Bool.False; Types.snd = Types.None })
136 (PolicyStep.jump_expansion_step program (Types.pi1 labels)
139 (** val measure_int :
140 ASM.labelled_instruction List.list -> PolicyFront.ppc_pc_map -> Nat.nat
142 let rec measure_int program policy acc =
145 | List.Cons (h, t) ->
146 (match (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
147 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
148 (Nat.S Nat.O))))))))))))))))
149 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
150 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
151 (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length t))
152 policy.Types.snd { Types.fst = Nat.O; Types.snd =
153 Assembly.Short_jump }).Types.snd with
154 | Assembly.Short_jump -> measure_int t policy acc
155 | Assembly.Absolute_jump ->
156 measure_int t policy (Nat.plus acc (Nat.S Nat.O))
157 | Assembly.Long_jump ->
158 measure_int t policy (Nat.plus acc (Nat.S (Nat.S Nat.O))))
160 (** val je_fixpoint :
161 ASM.labelled_instruction List.list Types.sig0 -> PolicyFront.ppc_pc_map
162 Types.option Types.sig0 **)
163 let je_fixpoint program =
165 (jump_expansion_internal program (Nat.S
166 (Nat.times (Nat.S (Nat.S Nat.O)) (List.length (Types.pi1 program)))))).Types.snd
168 (** val jump_expansion' :
169 ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word,
170 BitVector.word -> Bool.bool) Types.prod Types.sig0 Types.option **)
171 let jump_expansion' program =
172 let program' = program.ASM.code in
173 let f = Types.pi1 (je_fixpoint program') in
175 | Types.None -> (fun _ -> Types.None)
177 (fun _ -> Types.Some { Types.fst = (fun ppc ->
179 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
180 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
181 (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
182 Types.snd = Assembly.Short_jump }).Types.fst
184 (*prerr_endline "Z3";*)
185 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
186 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
187 (Nat.S Nat.O)))))))))))))))) pc); Types.snd = (fun ppc ->
189 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
190 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
191 (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
192 Types.snd = Assembly.Short_jump }).Types.snd
194 PolicyFront.jmpeqb jl Assembly.Long_jump) })) __