Changeset 1047 for src/RTLabs

Timestamp:

Jun 29, 2011, 5:38:27 PM (10 years ago)

Author:

mulligan

Message:

more work from today

File:

• src/RTLabs/RTLAbstoRTL.ma (modified) (6 diffs)

src/RTLabs/RTLAbstoRTL.ma

@@ -30 +30 @@
     ].
 
-axiom fresh_reg: rtl_internal_function → rtl_internal_function × register.
-
+axiom register_fresh: universe RegisterTag → register.
+
+definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝
+  λdef.
+    let r ≝ register_fresh (rtl_if_runiverse def) in
+    let locals ≝ r :: rtl_if_locals def in
+    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
+    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
+    let rtl_if_sig' ≝ rtl_if_sig def in
+    let rtl_if_result' ≝ rtl_if_result def in
+    let rtl_if_params' ≝ rtl_if_params def in
+    let rtl_if_locals' ≝ locals in
+    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
+    let rtl_if_graph' ≝ rtl_if_graph def in
+    let rtl_if_entry' ≝ rtl_if_entry def in
+    let rtl_if_exit' ≝ rtl_if_exit def in
+      〈mk_rtl_internal_function
+        rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' rtl_if_result'
+        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
+        rtl_if_entry' rtl_if_exit', r〉.
+        
 let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
   match n with
@@ -49 +68 @@
     | nil          ⇒ None (register × register)
     ]
-  | nil ⇒ None (register × register)
-  ].
+  | nil ⇒ None (register × register) (* registers are not an address *)
+  ].
+
+let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
+  match n with
+  [ O ⇒ [ ]
+  | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
+  ].
+
+definition choose_rest ≝
+  λA: Type[0].
+  λleft, right: list A.
+  match left with
+  [ nil ⇒
+    match right with
+    [ nil ⇒ None ?
+    | _ ⇒ Some ? right
+    ]
+  | _ ⇒ Some ? left
+  ].
+
+definition complete_regs ≝
+  λdef.
+  λsrcrs1.
+  λsrcrs2.
+  let nb_added ≝ abs ((length ? srcrs1) - (length ? srcrs2)) in
+  let 〈def, added_regs〉 ≝ fresh_regs def nb_added in
+    if gtb nb_added 0 then
+      〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
+    else
+      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
+
+definition size_of_sig_type ≝
+  λsig.
+  match sig with
+  [ ASTint isize sign ⇒
+    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
+      Some ? (isize' ÷ (nat_of_bitvector ? int_size))
+  | ASTfloat _ ⇒ None ?
+  | ASToffset ⇒ Some ? (nat_of_bitvector ? int_size)
+  | ASTptr rgn ⇒ Some ? (nat_of_bitvector ? ptr_size)
+  ].
+
+definition concrete_size ≝ .
+
+definition concrete_offset ≝ .
 
 inductive register_type: Type[0] ≝
@@ -246 +309 @@
   [ cast_int i ⇒
     match destrs with
-    [ nil ⇒ None ?
+    [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     | cons hd tl ⇒
       match tl with
@@ -253 +316 @@
       ]
     ]
-  | cast_addr_symbol id ⇒
+  | cast_addrsymbol id ⇒
     match destrs with
     [ nil ⇒ None ?
@@ -263 +326 @@
       ]
     ]
-  | cast_stack_offset off ⇒
+  | cast_offset off ⇒
     match destrs with
     [ nil ⇒ None ?
@@ -280 +343 @@
       ]
     ]
-  | cast_float f ⇒ None ?
+  | cast_stack ⇒ ?
+  | cast_sizeof size ⇒ ?
+  (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *)
   ].