Changeset 2827 for extracted/rTLabsToRTL.ml

Timestamp:

Mar 8, 2013, 9:07:28 PM (8 years ago)

Author:

sacerdot

Message:

Everything extracted again.

File:

• extracted/rTLabsToRTL.ml (modified) (10 diffs)

extracted/rTLabsToRTL.ml

@@ -150 +150 @@
     -> 'a1) -> register_type -> 'a1 **)
 let rec register_type_rect_Type4 h_register_int h_register_ptr = function
-| Register_int x_21002 -> h_register_int x_21002
-| Register_ptr (x_21004, x_21003) -> h_register_ptr x_21004 x_21003
+| Register_int x_21128 -> h_register_int x_21128
+| Register_ptr (x_21130, x_21129) -> h_register_ptr x_21130 x_21129
 
 (** val register_type_rect_Type5 :
@@ -157 +157 @@
     -> 'a1) -> register_type -> 'a1 **)
 let rec register_type_rect_Type5 h_register_int h_register_ptr = function
-| Register_int x_21008 -> h_register_int x_21008
-| Register_ptr (x_21010, x_21009) -> h_register_ptr x_21010 x_21009
+| Register_int x_21134 -> h_register_int x_21134
+| Register_ptr (x_21136, x_21135) -> h_register_ptr x_21136 x_21135
 
 (** val register_type_rect_Type3 :
@@ -164 +164 @@
     -> 'a1) -> register_type -> 'a1 **)
 let rec register_type_rect_Type3 h_register_int h_register_ptr = function
-| Register_int x_21014 -> h_register_int x_21014
-| Register_ptr (x_21016, x_21015) -> h_register_ptr x_21016 x_21015
+| Register_int x_21140 -> h_register_int x_21140
+| Register_ptr (x_21142, x_21141) -> h_register_ptr x_21142 x_21141
 
 (** val register_type_rect_Type2 :
@@ -171 +171 @@
     -> 'a1) -> register_type -> 'a1 **)
 let rec register_type_rect_Type2 h_register_int h_register_ptr = function
-| Register_int x_21020 -> h_register_int x_21020
-| Register_ptr (x_21022, x_21021) -> h_register_ptr x_21022 x_21021
+| Register_int x_21146 -> h_register_int x_21146
+| Register_ptr (x_21148, x_21147) -> h_register_ptr x_21148 x_21147
 
 (** val register_type_rect_Type1 :
@@ -178 +178 @@
     -> 'a1) -> register_type -> 'a1 **)
 let rec register_type_rect_Type1 h_register_int h_register_ptr = function
-| Register_int x_21026 -> h_register_int x_21026
-| Register_ptr (x_21028, x_21027) -> h_register_ptr x_21028 x_21027
+| Register_int x_21152 -> h_register_int x_21152
+| Register_ptr (x_21154, x_21153) -> h_register_ptr x_21154 x_21153
 
 (** val register_type_rect_Type0 :
@@ -185 +185 @@
     -> 'a1) -> register_type -> 'a1 **)
 let rec register_type_rect_Type0 h_register_int h_register_ptr = function
-| Register_int x_21032 -> h_register_int x_21032
-| Register_ptr (x_21034, x_21033) -> h_register_ptr x_21034 x_21033
+| Register_int x_21158 -> h_register_int x_21158
+| Register_ptr (x_21160, x_21159) -> h_register_ptr x_21160 x_21159
 
 (** val register_type_inv_rect_Type4 :
@@ -317 +317 @@
       Joint.joint_if_result = (Obj.magic ret'); Joint.joint_if_params =
       (Obj.magic params'); Joint.joint_if_stacksize =
-      def'.Joint.joint_if_stacksize; Joint.joint_if_code =
+      def'.Joint.joint_if_stacksize; Joint.joint_if_local_stacksize =
+      def'.Joint.joint_if_local_stacksize; Joint.joint_if_code =
       def'.Joint.joint_if_code; Joint.joint_if_entry =
       def'.Joint.joint_if_entry }
@@ -451 +452 @@
          let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
          List.Cons ((Joint.ADDRESS (id, (Obj.magic r1), (Obj.magic r2))),
-         List.Nil))
+         (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1),
+         (Obj.magic (Joint.psd_argument_from_reg r1)),
+         (Obj.magic
+           (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))),
+         (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2),
+         (Obj.magic (Joint.psd_argument_from_reg r2)),
+         (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
+         List.Nil))))))
      | FrontEndOps.Oaddrstack offset ->
        (fun _ _ ->
@@ -459 +467 @@
              (Obj.magic (RTL.Rtl_stack_address (r1, r2)))
            in
-          x), List.Nil))) __ __
+          x), (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic r1),
+         (Obj.magic (Joint.psd_argument_from_reg r1)),
+         (Obj.magic
+           (Joint.psd_argument_from_byte (Joint.byte_of_nat offset))))),
+         (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic r2),
+         (Obj.magic (Joint.psd_argument_from_reg r2)),
+         (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
+         List.Nil))))))) __ __
   in
   Bind_new.Bret l
@@ -1159 +1174 @@
   let luniverse' = def.RTLabs_syntax.f_labgen in
   let stack_size' = def.RTLabs_syntax.f_stacksize in
-  let entry' = def.RTLabs_syntax.f_entry in
+  let entry' = Types.pi1 def.RTLabs_syntax.f_entry in
   let init = { Joint.joint_if_luniverse = luniverse';
     Joint.joint_if_runiverse = runiverse'; Joint.joint_if_result =
     (Obj.magic List.Nil); Joint.joint_if_params = (Obj.magic List.Nil);
-    Joint.joint_if_stacksize = stack_size'; Joint.joint_if_code =
+    Joint.joint_if_stacksize = stack_size'; Joint.joint_if_local_stacksize =
+    stack_size'; Joint.joint_if_code =
     (Obj.magic
       (Identifiers.add PreIdentifiers.LabelTag
-        (Identifiers.empty_map PreIdentifiers.LabelTag) (Types.pi1 entry')
-        (Joint.Final Joint.RETURN))); Joint.joint_if_entry =
-    (Types.pi1 (Obj.magic entry')) }
+        (Identifiers.empty_map PreIdentifiers.LabelTag) entry' (Joint.Final
+        Joint.RETURN))); Joint.joint_if_entry = (Obj.magic entry') }
   in
   (let { Types.fst = init'; Types.snd = lenv } =