open Preamble
-open Assembly
-
open Status
-open Fetch
-
open BitVectorTrie
open String
-open Exp
-
-open Arithmetic
-
-open Vector
-
-open FoldStuff
-
-open BitVector
-
-open Extranat
-
open Integers
open AST
open Errors
-open Extralib
+open Lists
+
+open Positive
+
+open Identifiers
+
+open CostLabel
+
+open ASM
+
+open Exp
open Setoids
open Option
+open Extranat
+
+open Vector
+
+open FoldStuff
+
+open BitVector
+
+open Arithmetic
+
+open Fetch
+
+open Assembly
+
open Div_and_mod
open Jmeq
open Util
-open List
-
-open Lists
-
open Bool
open Relations
open Nat
-open Positive
+open List
open Hints_declaration
open Types
-open Identifiers
-
-open CostLabel
-
-open ASM
+open Extralib
open PolicyFront
Types.sig0 -> PolicyFront.ppc_pc_map Types.sig0 -> (Bool.bool,
PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **)
let jump_expansion_step program labels old_sigma =
- (let { Types.fst = final_added; Types.snd = final_policy } =
+ (let { Types.fst = ignore; Types.snd = res } =
Types.pi1
- (FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ acc ->
- (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } =
- Types.pi1 acc
+ (FoldStuff.foldl_strong (Types.pi1 program)
+ (fun prefix x tl _ prefixlens_acc ->
+ (let { Types.fst = prefixlens; Types.snd = acc } =
+ Types.pi1 prefixlens_acc
+ in
+ (fun _ ->
+ (let { Types.fst = prefixlen; Types.snd = bvprefixlen } = prefixlens
in
(fun _ ->
+ let bvSprefixlen =
+ Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S Nat.O)))))))))))))))) bvprefixlen
+ in
+ (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } = acc in
+ (fun _ ->
(let { Types.fst = label; Types.snd = instr } = x in
(fun _ ->
let add_instr =
match instr with
| ASM.Instruction i ->
PolicyFront.jump_expansion_step_instruction (Types.pi1 labels)
- (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) i
+ (Types.pi1 old_sigma) inc_pc_sigma prefixlen i
| ASM.Comment x0 -> Types.None
| ASM.Cost x0 -> Types.None
| ASM.Jmp j ->
Types.Some
(PolicyFront.select_jump_length (Types.pi1 labels)
- (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) j)
+ (Types.pi1 old_sigma) inc_pc_sigma prefixlen j)
| ASM.Jnz (x0, x1, x2) -> Types.None
| ASM.Call c ->
Types.Some
(PolicyFront.select_call_length (Types.pi1 labels)
- (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) c)
+ (Types.pi1 old_sigma) inc_pc_sigma prefixlen c)
| ASM.Mov (x0, x1, x2) -> Types.None
in
let { Types.fst = inc_pc; Types.snd = inc_sigma } = inc_pc_sigma in
let old_length =
(BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length prefix))
+ (Nat.S Nat.O)))))))))))))))) bvprefixlen
(Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
Assembly.Short_jump }).Types.snd
in
let old_Slength =
(BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
- (List.length prefix))) (Types.pi1 old_sigma).Types.snd
- { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd
+ (Nat.S Nat.O)))))))))))))))) bvSprefixlen
+ (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
+ Assembly.Short_jump }).Types.snd
in
let updated_sigma =
BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
- (List.length prefix))) { Types.fst = (Nat.plus inc_pc isize);
- Types.snd = old_Slength }
+ (Nat.S Nat.O)))))))))))))))) bvSprefixlen { Types.fst =
+ (Nat.plus inc_pc isize); Types.snd = old_Slength }
(BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S Nat.O))))))))))))))))
- (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
- (List.length prefix)) { Types.fst = inc_pc; Types.snd =
- new_length } inc_sigma)
+ (Nat.S Nat.O)))))))))))))))) bvprefixlen { Types.fst = inc_pc;
+ Types.snd = new_length } inc_sigma)
in
+ { Types.fst = { Types.fst = (Nat.S prefixlen); Types.snd =
+ (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S Nat.O)))))))))))))))) bvprefixlen) }; Types.snd =
{ Types.fst = new_added; Types.snd = { Types.fst =
- (Nat.plus inc_pc isize); Types.snd = updated_sigma } })) __)) __)
- { Types.fst = Nat.O; Types.snd = { Types.fst = Nat.O; Types.snd =
+ (Nat.plus inc_pc isize); Types.snd = updated_sigma } } })) __)) __))
+ __)) __) { Types.fst = { Types.fst = Nat.O; Types.snd =
+ (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+ Nat.O))))))))))))))))) }; Types.snd = { Types.fst = Nat.O;
+ Types.snd = { Types.fst = Nat.O; Types.snd =
(BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S Nat.O))))))))))))))))
(Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
Assembly.Short_jump }).Types.snd } (BitVectorTrie.Stub (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } })
+ (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } } })
in
(fun _ ->
+ (let { Types.fst = final_added; Types.snd = final_policy } = res in
+ (fun _ ->
(match Util.gtb final_policy.Types.fst
(Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
Types.None })
| Bool.False ->
(fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
- (Types.Some final_policy) })) __)) __
+ (Types.Some final_policy) })) __)) __)) __