X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=extracted%2FpolicyStep.ml;h=3d66283a6482f75c66be73a08526561a2426feb1;hb=d549e01e37d9b10e96f60e64a1814f5a9208e283;hp=ddc45e972de4e13ec6323beab9ecbb3733a61e8d;hpb=b4da02b8856ccc723c707618038f6a5c3bf223e2;p=pkg-cerco%2Facc-trusted.git

diff --git a/extracted/policyStep.ml b/extracted/policyStep.ml
index ddc45e9..3d66283 100644
--- a/extracted/policyStep.ml
+++ b/extracted/policyStep.ml
@@ -1,27 +1,11 @@
 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
@@ -40,7 +24,17 @@ open PreIdentifiers
 
 open Errors
 
-open Extralib
+open Lists
+
+open Positive
+
+open Identifiers
+
+open CostLabel
+
+open ASM
+
+open Exp
 
 open Setoids
 
@@ -48,6 +42,20 @@ open Monad
 
 open Option
 
+open Extranat
+
+open Vector
+
+open FoldStuff
+
+open BitVector
+
+open Arithmetic
+
+open Fetch
+
+open Assembly
+
 open Div_and_mod
 
 open Jmeq
@@ -56,17 +64,13 @@ open Russell
 
 open Util
 
-open List
-
-open Lists
-
 open Bool
 
 open Relations
 
 open Nat
 
-open Positive
+open List
 
 open Hints_declaration
 
@@ -78,11 +82,7 @@ open Logic
 
 open Types
 
-open Identifiers
-
-open CostLabel
-
-open ASM
+open Extralib
 
 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 =
-  (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
@@ -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
-             (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))))))))))))))))
@@ -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
-           (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
@@ -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.Some final_policy) })) __)) __
+       (Types.Some final_policy) })) __)) __)) __