Changeset 2286 for src/joint/SemanticUtils.ma

Timestamp:

Aug 2, 2012, 3:18:11 PM (9 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:

• src/joint/SemanticUtils.ma (modified) (2 diffs)

src/joint/SemanticUtils.ma

@@ -1 +1 @@
 include "joint/semantics.ma".
 include alias "common/Identifiers.ma".
+include "utilities/hide.ma".
+include "ASM/BitVectorTrie.ma".
+
+record hw_register_env : Type[0] ≝
+  { reg_env : BitVectorTrie beval 6
+  ; carry_bit : bebit
+  ; other_bit : bebit
+  }.
+
+definition empty_hw_register_env: hw_register_env ≝
+  mk_hw_register_env (Stub …) BBundef BBundef.
+
+include alias "ASM/BitVectorTrie.ma".
+
+definition hwreg_retrieve: hw_register_env → Register → beval ≝
+ λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
+
+definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
+ λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
+  (carry_bit env) (other_bit env).
+
+definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝
+λv,env.mk_hw_register_env (reg_env env) v (other_bit env).
+
+definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
+λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v.
+
 
 (*** Store/retrieve on pseudo-registers ***)
+include alias "common/Identifiers.ma".
 
 axiom BadRegister : String.
@@ -13 +41 @@
 (*** Store/retrieve on hardware registers ***)
 
-definition init_hw_register_env: address → hw_register_env ≝
- λaddr.
-  let 〈dpl,dph〉 ≝ addr in
+definition init_hw_register_env: xpointer → hw_register_env ≝
+ λsp.
+  let 〈dpl,dph〉 ≝
+    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
+    [ OK p ⇒ λ_.p
+    | _ ⇒ λprf.⊥
+    ] (refl …) in
   let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
    hwreg_store RegisterDPL dpl env.
-
-(****************************************************************************)
-
-definition graph_pointer_of_label0:
- pointer → label → Σp:pointer. ptype p = Code ≝
- λoldpc,l.
-  mk_pointer 
-   (mk_block Code (block_id (pblock oldpc))) (mk_offset (pos (word_of_identifier … l))). 
-// qed.
-
-definition graph_pointer_of_label:
- ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
- λ_.λ_.λ_.λoldpc,l.
-  OK ? (graph_pointer_of_label0 oldpc l). 
-
-definition graph_label_of_pointer: pointer → res label ≝
- λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
-
-(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
- But I can't use it directly because this one uses a concrete definition of
- pointer_of_label and it is used to istantiate the more_sem_params record
- where the abstract version is declared as a field. Is there a better way
- to organize the code? *)
-definition graph_succ_p: label → address → res address ≝
- λl,old.
-  do ptr ← pointer_of_address old ;
-  let newptr ≝ graph_pointer_of_label0 ptr l in
-  address_of_pointer newptr.
-
-axiom BadProgramCounter: String.
-
-definition graph_fetch_function:
- ∀params1,sem_params,globals.
-  genv … (graph_params params1 globals) →
-   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
- λparams1,sem_params,globals,ge,st.
-  do p ← code_pointer_of_address (pc … st) ;
-  let b ≝ pblock p in
-  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
-  match def with
-  [ Internal def' ⇒ OK … def'
-  | External _ ⇒ Error … [MSG BadProgramCounter]].
-
-definition graph_fetch_statement:
- ∀params1,sem_params,globals.
-  genv … (graph_params params1 globals) →
-   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
- λparams1,sem_params,globals,ge,st.
-  do p ← code_pointer_of_address (pc … st) ;
-  do f ← graph_fetch_function … ge st ;
-  do l ← graph_label_of_pointer p;
-  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
+@hide_prf
+normalize in prf; destruct(prf)
+qed.
+
+(******************************** GRAPHS **************************************)
+
+definition bitvector_from_pos :
+  ∀n.Pos → BitVector n ≝
+  λn,p.bitvector_of_Z n (Zpred (pos p)).
+
+definition pos_from_bitvector :
+  ∀n.BitVector n → Pos ≝
+  λn,v.
+  match Zsucc (Z_of_unsigned_bitvector n v)
+  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
+  with
+  [ OZ ⇒ λprf.⊥
+  | pos x ⇒ λ_. x
+  | neg x ⇒ λprf.⊥
+  ] (refl …).
+@hide_prf
+elim v in prf;
+[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
+
+lemma pos_pos_from_bitvector :
+  ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).
+#n #bv elim bv -n
+[ %
+| #n * #bv #IH [ % | @IH ]
+]
+qed.
+
+lemma bitvector_from_pos_from_bitvector :
+  ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.
+#n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector
+>Zpred_Zsucc //
+qed.
+
+lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.
+  (∀q,r.
+    ppos m = natp_plus (natp_times q (ppos n)) r →
+    natp_lt r n →
+    P (〈q,r〉)) →
+  P (divide m n).
+#P #m #n #H
+lapply (refl … (divide m n))
+cases (divide ??) in ⊢ (???%→%);
+#q #r #EQ elim (divide_ok … EQ) -EQ @H
+qed.
+
+lemma lt_divisor_to_eq_mod : ∀p,q : Pos.
+  p < q → \snd (divide p q) = ppos p.
+#p #q #H @divide_elim * [2: #quot ]
+* [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]
+@⊥ elim (lt_to_not_le ?? H) #H @H -H -H
+[ @(transitive_le … (quot*q)) ] /2 by /
+qed.
+
+lemma pos_from_bitvector_from_pos :
+  ∀n,p.
+  p ≤ two_power_nat n →
+  pos_from_bitvector n (bitvector_from_pos n p) = p.
+#n #p #H
+cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)
+[2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]
+>pos_pos_from_bitvector
+whd in match (bitvector_from_pos ??);
+>Z_of_unsigned_bitvector_of_Z
+cases p in H ⊢ %;
+[ #_ %
+|*: #p' #H
+  whd in match (Zpred ?);
+  whd in match (Z_two_power_nat ?);
+  whd in ⊢ (??(?%)?);
+  >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]
+  whd
+  <succ_pred_n try assumption % #ABS destruct(ABS)
+]
+qed.
+
+lemma pos_from_bitvector_max : ∀n,bv.
+  pos_from_bitvector n bv ≤ two_power_nat n.
+#n #bv
+change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)
+>pos_pos_from_bitvector
+@Zlt_to_Zle
+@bv_Z_unsigned_max
+qed.
+
+definition graph_offset_of_label : label → option offset ≝
+  λl.let p ≝ word_of_identifier … l in
+  if leb p (two_power_nat offset_size) then
+    return mk_offset (bitvector_from_pos … p)
+  else
+    None ?.
+
+definition graph_label_of_offset: offset → label ≝
+ λo.an_identifier ? (pos_from_bitvector ? (offv o)).
+
+definition make_sem_graph_params :
+  ∀pars : graph_params.
+  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
+  sem_params ≝
+  λpars,g_pars.
+  mk_sem_params
+    pars
+    (mk_more_sem_params
+      pars
+      g_pars
+      graph_offset_of_label
+      graph_label_of_offset
+      ??
+    ).
+whd in match graph_label_of_offset;
+whd in match graph_offset_of_label;
+whd in match word_of_identifier;
+normalize nodelta * #x
+@(leb_elim ? (two_power_nat ?)) normalize nodelta
+[ #_ >bitvector_from_pos_from_bitvector %
+| #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max
+| #H whd >(pos_from_bitvector_from_pos … H) %
+| #_ %
+]
+qed.
+
+(******************************** LINEAR **************************************)
+
+definition lin_offset_of_nat : ℕ → option offset ≝
+  λn.
+  if leb (S n) (2^offset_size) then
+    return mk_offset (bitvector_of_nat ? n)
+  else
+    None ?.
+
+definition lin_nat_of_offset : offset → ℕ ≝
+  λo.nat_of_bitvector ? (offv o).
+
+
+definition make_sem_lin_params :
+  ∀pars : lin_params.
+  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
+  sem_params ≝
+  λpars,g_pars.
+  mk_sem_params
+    pars
+    (mk_more_sem_params
+      pars
+      g_pars
+      lin_offset_of_nat
+      lin_nat_of_offset
+      ??
+    ).
+[ * ] #x
+whd in match lin_offset_of_nat;
+whd in match lin_nat_of_offset;
+normalize nodelta
+@leb_elim normalize nodelta #H
+[ >bitvector_of_nat_inverse_nat_of_bitvector %
+| @⊥ cases H #H @H -H -H //
+| whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) %
+| %
+]
+qed.