Imported Upstream version 0.2

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

diff --git a/extracted/policyStep.ml b/extracted/policyStep.ml
index ddc45e972de4e13ec6323beab9ecbb3733a61e8d..3d66283a6482f75c66be73a08526561a2426feb1 100644 (file)
--- a/extracted/policyStep.ml
+++ b/extracted/policyStep.ml
@@ -1,27 +1,11 @@
 open Preamble
 
 open Preamble
 

-open Assembly
-

 open Status
 
 open Status
 

-open Fetch
-

 open BitVectorTrie
 
 open String
 
 open BitVectorTrie
 
 open String
 

-open Exp
-
-open Arithmetic
-
-open Vector
-
-open FoldStuff
-
-open BitVector
-
-open Extranat
-

 open Integers
 
 open AST
 open Integers
 
 open AST


@@ -40,7 +24,17 @@ open PreIdentifiers
 
 open Errors
 
 
 open Errors
 

-open Extralib
+open Lists
+
+open Positive
+
+open Identifiers
+
+open CostLabel
+
+open ASM
+
+open Exp

 
 open Setoids
 
 
 open Setoids
 


@@ -48,6 +42,20 @@ open Monad
 
 open Option
 
 
 open Option
 

+open Extranat
+
+open Vector
+
+open FoldStuff
+
+open BitVector
+
+open Arithmetic
+
+open Fetch
+
+open Assembly
+

 open Div_and_mod
 
 open Jmeq
 open Div_and_mod
 
 open Jmeq


@@ -56,17 +64,13 @@ open Russell
 
 open Util
 
 
 open Util
 

-open List
-
-open Lists
-

 open Bool
 
 open Relations
 
 open Nat
 
 open Bool
 
 open Relations
 
 open Nat
 

-open Positive
+open List

 
 open Hints_declaration
 
 
 open Hints_declaration
 


@@ -78,11 +82,7 @@ open Logic
 
 open Types
 
 
 open Types
 

-open Identifiers
-
-open CostLabel
-
-open ASM
+open Extralib

 
 open PolicyFront
 
 
 open PolicyFront
 


@@ -91,41 +91,49 @@ 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 =
     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
      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 _ ->
           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)
          (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)
            | 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)
            | 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
            | 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
              (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
              Assembly.Short_jump }).Types.snd
          in


@@ -151,34 +159,31 @@ let jump_expansion_step program labels old_sigma =
          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
          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
          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
              (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
          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 =
          { 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))))))))))))))))
          (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))))))))))))))))


@@ -195,9 +200,11 @@ let jump_expansion_step program labels old_sigma =
              (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
              (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 _ ->
    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
   (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


@@ -207,5 +214,5 @@ let jump_expansion_step program labels old_sigma =
        Types.None })
    | Bool.False ->
      (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
        Types.None })
    | Bool.False ->
      (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =

-       (Types.Some final_policy) })) __)) __
+       (Types.Some final_policy) })) __)) __)) __