Changeset 1415 for src/LIN

Timestamp:

Oct 19, 2011, 4:22:52 PM (8 years ago)

Author:

sacerdot

Message:

1. hwreg_store/retrieve no longer returns a res (but it is still axiomatized)
2. added initialization of local environment that sets the sp in the appropriate way
3. ASM/I8051 splitted into ASM/I8051bis because of some bugs with disambiguation

File:

• src/LIN/joint_LTL_LIN_semantics.ma (modified) (2 diffs)

src/LIN/joint_LTL_LIN_semantics.ma

@@ -1 +1 @@
 include "LIN/joint_LTL_LIN.ma".
 include "joint/SemanticUtils.ma".
+
+definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
+definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
 
 (*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
@@ -6 +9 @@
  λsuccT,succ,pointer_of_label.
  mk_more_sem_params ?
-  unit it hw_register_env empty_hw_register_env 0 it succ
-   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
-    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
-    (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)
-    (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)
+  unit it hw_register_env init_hw_register_env 0 it succ
+   hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA)
+    (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB)
+    (λ_.hw_reg_store RegisterDPL) (λe.λ_.hw_reg_retrieve e RegisterDPL)
+    (λ_.hw_reg_store RegisterDPH) (λe.λ_.hw_reg_retrieve e RegisterDPH)
      (λlocals,dest_src.
        match dest_src with
        [ from_acc reg ⇒
-          do v ← hwreg_retrieve locals RegisterA ;
-          hwreg_store reg v locals
+          do v ← hw_reg_retrieve locals RegisterA ;
+          hw_reg_store reg v locals
        | to_acc reg ⇒
-          do v ← hwreg_retrieve locals reg ;
-          hwreg_store RegisterA v locals ])
+          do v ← hw_reg_retrieve locals reg ;
+          hw_reg_store RegisterA v locals ])
      pointer_of_label.