Changeset 2746 for extracted

Timestamp:

Feb 27, 2013, 10:46:33 PM (7 years ago)

Author:

sacerdot

Message:

1. debugging code in glue
2. updated version

Location:

extracted

Files:

• compiler.ml (modified) (2 diffs)
• compiler.mli (modified) (1 diff)
• policy.ml (modified) (2 diffs)
• untrusted/glue.ml (modified) (1 diff)
• untrusted/glue.mli (modified) (1 diff)

extracted/compiler.ml

@@ -337 +337 @@
 open ASMCostsSplit
 
+type strong_decidable = (__, __) Types.sum
+
+(** val strong_decidable_in_codomain :
+    Deqsets.deqSet -> Nat.nat -> __ BitVectorTrie.bitVectorTrie -> __ ->
+    strong_decidable **)
+let strong_decidable_in_codomain a0 n m =
+  BitVectorTrie.bitVectorTrie_rect_Type0 (fun a' a1 ->
+    Bool.bool_inv_rect_Type0 (Deqsets.eqb a0 a' a1) (fun _ -> Types.Inl __)
+      (fun _ -> Types.Inr __)) (fun n0 l r hl hr a1 ->
+    match hl a1 with
+    | Types.Inl _ -> Types.Inl __
+    | Types.Inr _ ->
+      (match hr a1 with
+       | Types.Inl _ -> Types.Inl __
+       | Types.Inr _ -> Types.Inr __)) (fun n0 a1 -> Types.Inr __) n m
+
 (** val compile :
     Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
@@ -351 +367 @@
         let k' =
           lift_cost_map_back_to_front p'
-            (Fetch.load_code_memory p4.Types.fst) p4.Types.snd (assert false
-            (* absurd case *)) k
+            (Fetch.load_code_memory p4.Types.fst) p4.Types.snd
+            (Obj.magic
+              (strong_decidable_in_codomain
+                (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.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)))))))))))))))) (Obj.magic p4).Types.snd)) k
         in
         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p4;

extracted/compiler.mli

@@ -295 +295 @@
 open ASMCostsSplit
 
+type strong_decidable = (__, __) Types.sum
+
+val strong_decidable_in_codomain :
+  Deqsets.deqSet -> Nat.nat -> __ BitVectorTrie.bitVectorTrie -> __ ->
+  strong_decidable
+
 val compile :
   Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,

extracted/policy.ml

@@ -101 +101 @@
    | Nat.S m ->
      (fun _ ->
-       (let { Types.fst = no_ch; Types.snd = z } =
-          Types.pi1 (jump_expansion_internal program0 m)
-        in
+       let res1 = Types.pi1 (jump_expansion_internal program0 m) in
+       (let { Types.fst = no_ch; Types.snd = z } = res1 in
        (fun _ ->
        (match z with
@@ -111 +110 @@
           (fun _ ->
             match no_ch with
-            | Bool.True -> Types.pi1 (jump_expansion_internal program0 m)
+            | Bool.True -> res1
             | Bool.False ->
               Types.pi1

extracted/untrusted/glue.ml

@@ -26 +26 @@
  else if n < 0 then assert false
  else Nat.S (matitanat_of_int (n-1))
+
+let rec int_of_matitanat =
+ function
+    Nat.O -> 0
+  | Nat.S n -> int_of_matitanat n + 1

extracted/untrusted/glue.mli

@@ -6 +6 @@
 
 val matitanat_of_int : int -> Nat.nat
+
+val int_of_matitanat : Nat.nat -> int