Changeset 2286 for src/LIN/semantics.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/semantics.ma

    r1601 r2286  
    22include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 definition lin_succ_pc: unit → address → res address :=
    5  λ_.λaddr. addr_add addr 1.
    6 
    7 axiom BadOldPointer: String.
    8 (*CSC: XXX factorize the code with graph_fetch_function!!! *)
    9 definition lin_fetch_function:
    10  ∀globals. genv … (lin_params globals) → pointer → res (joint_internal_function globals (lin_params globals)) ≝
    11  λglobals,ge,old.
    12   let b ≝ pblock old in
    13   do def ← opt_to_res ? [MSG BadOldPointer] (find_funct_ptr … ge b);
    14   match def with
    15   [ Internal fn ⇒ OK … fn
    16   | External _ ⇒ Error … [MSG BadOldPointer]].
    17 
    18 axiom BadLabel: String.
    19 definition lin_pointer_of_label:
    20  ∀globals. genv … (lin_params globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
    21  λglobals,ge,old,l.
    22   do fn ← lin_fetch_function … ge old ;
    23   do pos ←
    24    opt_to_res ? [MSG BadLabel]
    25     (position_of ?
    26       (λs. let 〈l',x〉 ≝ s in
    27         match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
    28      (joint_if_code … (lin_params …) fn)) ;
    29   OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
    30 // qed.
    31 
    32 (*CSC: XXX factorize code with graph_fetch_statement?*)
    33 axiom BadProgramCounter: String.
    34 definition lin_fetch_statement:
    35  ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params unit) → res (pre_lin_statement globals) ≝
    36  λglobals,ge,st.
    37   do ppc ← pointer_of_address (pc … st) ;
    38   do fn ← lin_fetch_function … ge ppc ;
    39   let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
    40   do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
    41   OK … (\snd found).
    42 
    43 definition lin_fullexec: fullexec io_out io_in ≝
    44  ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement lin_pointer_of_label.
     4definition LIN_semantics : sem_params ≝
     5  make_sem_lin_params LIN (LTL_LIN_semantics ?).
Note: See TracChangeset for help on using the changeset viewer.