75 open Hints_declaration
89 (** val jump_expansion_step :
90 ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map
91 Types.sig0 -> PolicyFront.ppc_pc_map Types.sig0 -> (Bool.bool,
92 PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **)
93 let jump_expansion_step program labels old_sigma =
94 (let { Types.fst = ignore; Types.snd = res } =
96 (FoldStuff.foldl_strong (Types.pi1 program)
97 (fun prefix x tl _ prefixlens_acc ->
98 (let { Types.fst = prefixlens; Types.snd = acc } =
99 Types.pi1 prefixlens_acc
102 (let { Types.fst = prefixlen; Types.snd = bvprefixlen } = prefixlens
106 Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
107 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
108 (Nat.S Nat.O)))))))))))))))) bvprefixlen
110 (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } = acc in
112 (let { Types.fst = label; Types.snd = instr } = x in
116 | ASM.Instruction i ->
117 PolicyFront.jump_expansion_step_instruction (Types.pi1 labels)
118 (Types.pi1 old_sigma) inc_pc_sigma prefixlen i
119 | ASM.Comment x0 -> Types.None
120 | ASM.Cost x0 -> Types.None
123 (PolicyFront.select_jump_length (Types.pi1 labels)
124 (Types.pi1 old_sigma) inc_pc_sigma prefixlen j)
125 | ASM.Jnz (x0, x1, x2) -> Types.None
128 (PolicyFront.select_call_length (Types.pi1 labels)
129 (Types.pi1 old_sigma) inc_pc_sigma prefixlen c)
130 | ASM.Mov (x0, x1, x2) -> Types.None
132 let { Types.fst = inc_pc; Types.snd = inc_sigma } = inc_pc_sigma in
134 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
135 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
136 (Nat.S Nat.O)))))))))))))))) bvprefixlen
137 (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
138 Assembly.Short_jump }).Types.snd
140 let old_size = PolicyFront.instruction_size_jmplen old_length instr
142 let { Types.fst = new_length; Types.snd = isize } =
145 { Types.fst = Assembly.Short_jump; Types.snd =
146 (PolicyFront.instruction_size_jmplen Assembly.Short_jump
149 { Types.fst = (PolicyFront.max_length old_length pl);
151 (PolicyFront.instruction_size_jmplen
152 (PolicyFront.max_length old_length pl) instr) }
156 | Types.None -> inc_added
157 | Types.Some x0 -> Nat.plus inc_added (Nat.minus isize old_size)
160 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
161 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
162 (Nat.S Nat.O)))))))))))))))) bvSprefixlen
163 (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
164 Assembly.Short_jump }).Types.snd
167 BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
168 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
169 (Nat.S Nat.O)))))))))))))))) bvSprefixlen { Types.fst =
170 (Nat.plus inc_pc isize); Types.snd = old_Slength }
171 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
172 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
173 (Nat.S Nat.O)))))))))))))))) bvprefixlen { Types.fst = inc_pc;
174 Types.snd = new_length } inc_sigma)
176 { Types.fst = { Types.fst = (Nat.S prefixlen); Types.snd =
177 (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
178 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
179 (Nat.S Nat.O)))))))))))))))) bvprefixlen) }; Types.snd =
180 { Types.fst = new_added; Types.snd = { Types.fst =
181 (Nat.plus inc_pc isize); Types.snd = updated_sigma } } })) __)) __))
182 __)) __) { Types.fst = { Types.fst = Nat.O; Types.snd =
183 (BitVector.zero (Nat.S (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.O))))))))))))))))) }; Types.snd = { Types.fst = Nat.O;
186 Types.snd = { Types.fst = Nat.O; Types.snd =
187 (BitVectorTrie.insert (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))))))))))))))))
190 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
191 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
192 (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O;
194 (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
195 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
196 (Nat.S Nat.O))))))))))))))))
197 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
198 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
199 (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O)
200 (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
201 Assembly.Short_jump }).Types.snd } (BitVectorTrie.Stub (Nat.S
202 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
203 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } } })
206 (let { Types.fst = final_added; Types.snd = final_policy } = res in
208 (match Util.gtb final_policy.Types.fst
209 (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
210 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
211 (Nat.S (Nat.S Nat.O))))))))))))))))) with
213 (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
216 (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
217 (Types.Some final_policy) })) __)) __)) __