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/joint/SemanticUtils.ma

    r2176 r2286  
    11include "joint/semantics.ma".
    22include alias "common/Identifiers.ma".
     3include "utilities/hide.ma".
     4include "ASM/BitVectorTrie.ma".
     5
     6record hw_register_env : Type[0] ≝
     7  { reg_env : BitVectorTrie beval 6
     8  ; carry_bit : bebit
     9  ; other_bit : bebit
     10  }.
     11
     12definition empty_hw_register_env: hw_register_env ≝
     13  mk_hw_register_env (Stub …) BBundef BBundef.
     14
     15include alias "ASM/BitVectorTrie.ma".
     16
     17definition hwreg_retrieve: hw_register_env → Register → beval ≝
     18 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
     19
     20definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
     21 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
     22  (carry_bit env) (other_bit env).
     23
     24definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝
     25λv,env.mk_hw_register_env (reg_env env) v (other_bit env).
     26
     27definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
     28λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v.
     29
    330
    431(*** Store/retrieve on pseudo-registers ***)
     32include alias "common/Identifiers.ma".
    533
    634axiom BadRegister : String.
     
    1341(*** Store/retrieve on hardware registers ***)
    1442
    15 definition init_hw_register_env: address → hw_register_env ≝
    16  λaddr.
    17   let 〈dpl,dph〉 ≝ addr in
     43definition init_hw_register_env: xpointer → hw_register_env ≝
     44 λsp.
     45  let 〈dpl,dph〉 ≝
     46    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
     47    [ OK p ⇒ λ_.p
     48    | _ ⇒ λprf.⊥
     49    ] (refl …) in
    1850  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
    1951   hwreg_store RegisterDPL dpl env.
    20 
    21 (****************************************************************************)
    22 
    23 definition graph_pointer_of_label0:
    24  pointer → label → Σp:pointer. ptype p = Code ≝
    25  λoldpc,l.
    26   mk_pointer
    27    (mk_block Code (block_id (pblock oldpc))) (mk_offset (pos (word_of_identifier … l))).
    28 // qed.
    29 
    30 definition graph_pointer_of_label:
    31  ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
    32  λ_.λ_.λ_.λoldpc,l.
    33   OK ? (graph_pointer_of_label0 oldpc l).
    34 
    35 definition graph_label_of_pointer: pointer → res label ≝
    36  λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
    37 
    38 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    39  But I can't use it directly because this one uses a concrete definition of
    40  pointer_of_label and it is used to istantiate the more_sem_params record
    41  where the abstract version is declared as a field. Is there a better way
    42  to organize the code? *)
    43 definition graph_succ_p: label → address → res address ≝
    44  λl,old.
    45   do ptr ← pointer_of_address old ;
    46   let newptr ≝ graph_pointer_of_label0 ptr l in
    47   address_of_pointer newptr.
    48 
    49 axiom BadProgramCounter: String.
    50 
    51 definition graph_fetch_function:
    52  ∀params1,sem_params,globals.
    53   genv … (graph_params params1 globals) →
    54    state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
    55  λparams1,sem_params,globals,ge,st.
    56   do p ← code_pointer_of_address (pc … st) ;
    57   let b ≝ pblock p in
    58   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    59   match def with
    60   [ Internal def' ⇒ OK … def'
    61   | External _ ⇒ Error … [MSG BadProgramCounter]].
    62 
    63 definition graph_fetch_statement:
    64  ∀params1,sem_params,globals.
    65   genv … (graph_params params1 globals) →
    66    state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
    67  λparams1,sem_params,globals,ge,st.
    68   do p ← code_pointer_of_address (pc … st) ;
    69   do f ← graph_fetch_function … ge st ;
    70   do l ← graph_label_of_pointer p;
    71   opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
     52@hide_prf
     53normalize in prf; destruct(prf)
     54qed.
     55
     56(******************************** GRAPHS **************************************)
     57
     58definition bitvector_from_pos :
     59  ∀n.Pos → BitVector n ≝
     60  λn,p.bitvector_of_Z n (Zpred (pos p)).
     61
     62definition pos_from_bitvector :
     63  ∀n.BitVector n → Pos ≝
     64  λn,v.
     65  match Zsucc (Z_of_unsigned_bitvector n v)
     66  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
     67  with
     68  [ OZ ⇒ λprf.⊥
     69  | pos x ⇒ λ_. x
     70  | neg x ⇒ λprf.⊥
     71  ] (refl …).
     72@hide_prf
     73elim v in prf;
     74[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
     75
     76lemma pos_pos_from_bitvector :
     77  ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).
     78#n #bv elim bv -n
     79[ %
     80| #n * #bv #IH [ % | @IH ]
     81]
     82qed.
     83
     84lemma bitvector_from_pos_from_bitvector :
     85  ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.
     86#n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector
     87>Zpred_Zsucc //
     88qed.
     89
     90lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.
     91  (∀q,r.
     92    ppos m = natp_plus (natp_times q (ppos n)) r →
     93    natp_lt r n →
     94    P (〈q,r〉)) →
     95  P (divide m n).
     96#P #m #n #H
     97lapply (refl … (divide m n))
     98cases (divide ??) in ⊢ (???%→%);
     99#q #r #EQ elim (divide_ok … EQ) -EQ @H
     100qed.
     101
     102lemma lt_divisor_to_eq_mod : ∀p,q : Pos.
     103  p < q → \snd (divide p q) = ppos p.
     104#p #q #H @divide_elim * [2: #quot ]
     105* [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]
     106@⊥ elim (lt_to_not_le ?? H) #H @H -H -H
     107[ @(transitive_le … (quot*q)) ] /2 by /
     108qed.
     109
     110lemma pos_from_bitvector_from_pos :
     111  ∀n,p.
     112  p ≤ two_power_nat n →
     113  pos_from_bitvector n (bitvector_from_pos n p) = p.
     114#n #p #H
     115cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)
     116[2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]
     117>pos_pos_from_bitvector
     118whd in match (bitvector_from_pos ??);
     119>Z_of_unsigned_bitvector_of_Z
     120cases p in H ⊢ %;
     121[ #_ %
     122|*: #p' #H
     123  whd in match (Zpred ?);
     124  whd in match (Z_two_power_nat ?);
     125  whd in ⊢ (??(?%)?);
     126  >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]
     127  whd
     128  <succ_pred_n try assumption % #ABS destruct(ABS)
     129]
     130qed.
     131
     132lemma pos_from_bitvector_max : ∀n,bv.
     133  pos_from_bitvector n bv ≤ two_power_nat n.
     134#n #bv
     135change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)
     136>pos_pos_from_bitvector
     137@Zlt_to_Zle
     138@bv_Z_unsigned_max
     139qed.
     140
     141definition graph_offset_of_label : label → option offset ≝
     142  λl.let p ≝ word_of_identifier … l in
     143  if leb p (two_power_nat offset_size) then
     144    return mk_offset (bitvector_from_pos … p)
     145  else
     146    None ?.
     147
     148definition graph_label_of_offset: offset → label ≝
     149 λo.an_identifier ? (pos_from_bitvector ? (offv o)).
     150
     151definition make_sem_graph_params :
     152  ∀pars : graph_params.
     153  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
     154  sem_params ≝
     155  λpars,g_pars.
     156  mk_sem_params
     157    pars
     158    (mk_more_sem_params
     159      pars
     160      g_pars
     161      graph_offset_of_label
     162      graph_label_of_offset
     163      ??
     164    ).
     165whd in match graph_label_of_offset;
     166whd in match graph_offset_of_label;
     167whd in match word_of_identifier;
     168normalize nodelta * #x
     169@(leb_elim ? (two_power_nat ?)) normalize nodelta
     170[ #_ >bitvector_from_pos_from_bitvector %
     171| #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max
     172| #H whd >(pos_from_bitvector_from_pos … H) %
     173| #_ %
     174]
     175qed.
     176
     177(******************************** LINEAR **************************************)
     178
     179definition lin_offset_of_nat : ℕ → option offset ≝
     180  λn.
     181  if leb (S n) (2^offset_size) then
     182    return mk_offset (bitvector_of_nat ? n)
     183  else
     184    None ?.
     185
     186definition lin_nat_of_offset : offset → ℕ ≝
     187  λo.nat_of_bitvector ? (offv o).
     188
     189
     190definition make_sem_lin_params :
     191  ∀pars : lin_params.
     192  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
     193  sem_params ≝
     194  λpars,g_pars.
     195  mk_sem_params
     196    pars
     197    (mk_more_sem_params
     198      pars
     199      g_pars
     200      lin_offset_of_nat
     201      lin_nat_of_offset
     202      ??
     203    ).
     204[ * ] #x
     205whd in match lin_offset_of_nat;
     206whd in match lin_nat_of_offset;
     207normalize nodelta
     208@leb_elim normalize nodelta #H
     209[ >bitvector_of_nat_inverse_nat_of_bitvector %
     210| @⊥ cases H #H @H -H -H //
     211| whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) %
     212| %
     213]
     214qed.
Note: See TracChangeset for help on using the changeset viewer.