Merge tag 'upstream/0.2'

[pkg-cerco/acc-trusted.git] / extracted / policyFront.ml

diff --git a/extracted/policyFront.ml b/extracted/policyFront.ml
index 1b8ccc5fe5613cdcc70c7ef37441965710097541..66d8985dadf91fd8c3afb6d8b17563dea5f5bd2f 100644 (file)
--- a/extracted/policyFront.ml
+++ b/extracted/policyFront.ml
@@ -1,86 +1,86 @@
 open Preamble
 
-open BitVectorTrie
+open Div_and_mod
 
-open String
+open Jmeq
 
-open Exp
+open Russell
 
-open Arithmetic
+open Util
 
-open Vector
+open Bool
 
-open FoldStuff
+open Relations
 
-open BitVector
+open Nat
 
-open Extranat
+open List
 
-open Integers
+open Hints_declaration
 
-open AST
+open Core_notation
 
-open LabelledObjects
+open Pts
 
-open Proper
+open Logic
 
-open PositiveMap
+open Types
 
-open Deqsets
+open Extralib
 
-open ErrorMessages
+open Status
 
-open PreIdentifiers
+open BitVectorTrie
 
-open Errors
+open String
 
-open Extralib
+open Integers
 
-open Setoids
+open AST
 
-open Monad
+open LabelledObjects
 
-open Option
+open Proper
 
-open Div_and_mod
+open PositiveMap
 
-open Jmeq
+open Deqsets
 
-open Russell
+open ErrorMessages
 
-open Util
+open PreIdentifiers
 
-open List
+open Errors
 
 open Lists
 
-open Bool
+open Positive
 
-open Relations
+open Identifiers
 
-open Nat
+open CostLabel
 
-open Positive
+open ASM
 
-open Hints_declaration
+open Exp
 
-open Core_notation
+open Setoids
 
-open Pts
+open Monad
 
-open Logic
+open Option
 
-open Types
+open Extranat
 
-open Identifiers
+open Vector
 
-open CostLabel
+open FoldStuff
 
-open ASM
+open BitVector
 
-open Fetch
+open Arithmetic
 
-open Status
+open Fetch
 
 open Assembly
 
@@ -656,34 +656,46 @@ let jump_expansion_step_instruction labels old_sigma inc_sigma ppc i =
     ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
     ppc_pc_map Types.option Types.sig0 **)
 let jump_expansion_start program labels =
-  let final_policy =
-    FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ p ->
-      let { Types.fst = pc; Types.snd = sigma } = Types.pi1 p in
-      let { Types.fst = label; Types.snd = instr } = x in
-      let isize = instruction_size_jmplen Assembly.Short_jump instr in
-      { Types.fst = (Nat.plus pc isize); 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))))))))))))))))
-        (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 pc isize); Types.snd = Assembly.Short_jump }
-        sigma) }) { 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))))))))))))))))
-        (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.O) { Types.fst = Nat.O;
-        Types.snd = Assembly.Short_jump } (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)))))))))))))))))) }
-  in
-  (match Util.gtb (Types.pi1 final_policy).Types.fst
+  (let { Types.fst = ignore; Types.snd = final_policy } =
+     Types.pi1
+       (FoldStuff.foldl_strong (Types.pi1 program)
+         (fun prefix x tl _ acc_pol ->
+         (let { Types.fst = acc; Types.snd = p } = Types.pi1 acc_pol in
+         (fun _ ->
+         let { Types.fst = pc; Types.snd = sigma } = p in
+         let { Types.fst = label; Types.snd = instr } = x in
+         let isize = instruction_size_jmplen Assembly.Short_jump instr in
+         let sacc =
+           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)))))))))))))))) acc
+         in
+         { Types.fst = sacc; Types.snd = { Types.fst = (Nat.plus pc isize);
+         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)))))))))))))))) sacc { Types.fst =
+           (Nat.plus pc isize); Types.snd = Assembly.Short_jump } sigma) } }))
+           __) { Types.fst =
+         (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 =
+         (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.O) { Types.fst = Nat.O;
+           Types.snd = Assembly.Short_jump } (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)))))))))))))))))) } })
+   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
              (Nat.S (Nat.S Nat.O))))))))))))))))) with
    | Bool.True -> (fun _ -> Types.None)
-   | Bool.False -> (fun _ -> Types.Some (Types.pi1 final_policy))) __
+   | Bool.False -> (fun _ -> Types.Some final_policy)) __)) __