Changeset 1308 for src/RTLabs/RTLAbstoRTL.ma

Timestamp:

Oct 6, 2011, 5:27:32 PM (8 years ago)

Author:

mulligan

Message:

changes to translate_cst

File:

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

src/RTLabs/RTLAbstoRTL.ma

@@ -127 +127 @@
   λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
 
+axiom split_into_bytes:
+  ∀size.
+  ∀int: bvint size.
+    Σbytes: list Byte. |bytes| = size_intsize size.
+
+lemma eqb_implies_eq:
+  ∀m, n: nat.
+    eqb m n = true → m = n.
+  #M
+  elim M
+  [1: #N normalize
+      cases N
+      [1: normalize //
+      |2: #M' normalize #HYP destruct(HYP)
+      ]
+  |2: #M' #IND_HYP #N
+      normalize
+      cases N
+      [1: normalize #HYP destruct(HYP)
+      |2: #M'' normalize #HYP
+          @eq_f @(IND_HYP M'')
+          assumption
+      ]
+   ]
+qed.
+
 let rec translate_cst
   (globals: list ident) (cst: constant) (destrs: list register)
@@ -134 +160 @@
   [ Ointconst size const ⇒
     match destrs with
-    [ nil        ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
-    | cons hd tl ⇒ ?
+    [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
+    | _   ⇒
+      let size' ≝ size_intsize size in
+        match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
+        [ true  ⇒ λgood_case.
+          match split_into_bytes size const with
+          [ dp bytes bytes_length_proof ⇒
+            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
+              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
+          ]
+        | false ⇒ λbad_case. ?
+        ] (refl … (eqb size' (|destrs|)))
     ]
   | Ofloatconst float ⇒ ⊥
-  | Oaddrsymbol id offset ⇒ ?
-  | Oaddrstack offset ⇒ ?
-  ].
-  [5: cases not_implemented (* XXX: float, error_float in o'caml *)
+  | Oaddrsymbol id offset ⇒
+    let 〈r1, r2〉 ≝ make_addr … destrs ? in
+      add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def
+  | Oaddrstack offset ⇒
+    let 〈r1, r2〉 ≝ make_addr … destrs ? in
+      add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def
+  ].
+  [1: >bytes_length_proof
+      cut(size' = |destrs|)
+      [1: @eqb_implies_eq
+          assumption
+      |2: #EQ_HYP
+          <EQ_HYP %
+      ]
+  |5: cases not_implemented (* XXX: float, error_float in o'caml *)
   ].