Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (7 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/common/ByteValues.ma

    r2275 r2286  
    44
    55include "common/Pointers.ma".
    6 include "ASM/I8051.ma".
    7 include "ASM/BitVectorTrie.ma".
     6include "utilities/hide.ma".
    87
    98record part (*r: region*): Type[0] ≝
     
    2221  - the [BVundef] value denoting an arbitrary bit pattern, such as the
    2322    value of an uninitialized variable
     23  - the [BVnonzero] value denoting an arbitrary but non-zero bit pattern,
     24    which arise in the RTLabs → RTL pass when translating equality comparisons
     25    between pointers (which get translated to multiple XORs between pointer
     26    parts).   
    2427*)
    2528
    2629inductive beval: Type[0] ≝
    2730  | BVundef: beval
     31  | BVnonzero: beval
    2832  | BVByte: Byte → beval
    2933  | BVnull: (*∀r:region.*) part  → beval
    30   | BVptr: ∀p:pointer. part (*ptype p*) → beval.
     34  | BVptr: block → ∀p:part.Vector Byte (S p) → beval.
    3135
    3236definition eq_beval: beval → beval → bool ≝
     
    3438  match v1 with
    3539   [ BVundef      ⇒ match v2 with [ BVundef      ⇒ true                           | _ ⇒ false ]
     40   | BVnonzero    ⇒ match v2 with [ BVnonzero    ⇒ true                           | _ ⇒ false ]
    3641   | BVByte b1    ⇒ match v2 with [ BVByte b2    ⇒ eq_bv … b1 b2                  | _ ⇒ false ]
    3742   | BVnull p1    ⇒ match v2 with [ BVnull p2    ⇒ eqb p1 p2                      | _ ⇒ false ]
    38    | BVptr P1 p1  ⇒ match v2 with [ BVptr P2 p2  ⇒ eq_pointer … P1 P2 ∧ eqb p1 p2 | _ ⇒ false ]].
    39 
    40 axiom CorruptedValue: String.
    41 
    42 let rec pointer_of_bevals_aux (p:pointer) (part: nat) (l: list beval) on l : res pointer ≝
     43   | BVptr b1 p1 o1  ⇒
     44      match v2 with
     45      [ BVptr b2 p2 o2  ⇒
     46        eq_block … b1 b2 ∧ eqb p1 p2 ∧
     47          (* equivalent to equality if p1 = p2 *)
     48          vprefix … (eq_bv 8) o1 o2
     49      | _ ⇒ false
     50      ]
     51   ].
     52
     53include alias "arithmetics/nat.ma".
     54
     55axiom CorruptedPointer: String.
     56
     57let rec pointer_of_bevals_aux (b:block) (part: nat) (acc : BitVector (part*8))
     58  (l: list beval) on l : res pointer ≝
    4359 match l with
    4460  [ nil ⇒
    45      if eqb part (size_pointer (*ptype p*)) then
    46       OK … p
     61     If eqb part (size_pointer (*ptype p*)) then with prf do
     62      return mk_pointer b (mk_offset (acc⌈BitVector (part*8)↦?⌉))
    4763     else
    48       Error … [MSG CorruptedValue]
     64      Error … [MSG CorruptedPointer]
    4965  | cons v tl ⇒
    5066     match v with
    51       [ BVptr p' part' ⇒
    52          if eq_pointer p p' ∧ eqb part part' then
    53           pointer_of_bevals_aux p (S part) tl
     67      [ BVptr b' part' o' ⇒
     68        let acc' ≝ vflatten … o' in
     69        if eq_block b b' ∧
     70           eqb part part' ∧
     71           vsuffix … eq_b acc acc' then
     72           pointer_of_bevals_aux b (S part') acc' tl
    5473         else
    55           Error … [MSG CorruptedValue]
    56       | _ ⇒ Error … [MSG CorruptedValue]]].
    57 
    58 axiom NotAPointer: String.
     74          Error … [MSG CorruptedPointer]
     75      | _ ⇒ Error … [MSG CorruptedPointer]
     76      ]
     77  ].
     78  @hide_prf
     79  >commutative_times_fast
     80  lapply prf @(eqb_elim part) #H * >H % qed.
    5981
    6082(* CSC: use vectors in place of lists? Or even better products of tuples
     
    6385 λl.
    6486 match l with
    65   [ nil ⇒ Error … [MSG NotAPointer]
     87  [ nil ⇒ Error … [MSG CorruptedPointer]
    6688  | cons he tl ⇒
    6789     match he with
    68       [ BVptr p part ⇒
    69          if eqb part 0 then pointer_of_bevals_aux p 1 tl else Error … [MSG NotAPointer]
    70       | _ ⇒ Error … [MSG NotAPointer]]].
     90      [ BVptr b part o ⇒
     91         if eqb part 0 then
     92           pointer_of_bevals_aux b (S part) (vflatten … o) tl
     93         else Error … [MSG CorruptedPointer]
     94      | _ ⇒ Error … [MSG CorruptedPointer]
     95      ]
     96  ].
    7197
    7298(* CSC: use vectors in place of lists? Or even better products of tuples
    7399   (more easily pattern matchable in the finite case)? *)
    74 let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) (pr: plus part n = size_pointer (*ptype p*)) on n: list beval ≝
     100let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) on n: n + part = size_pointer (*ptype p*) → list beval ≝
    75101 match n with
    76102  [ O ⇒ λ_.[]
    77   | S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n).
    78 <pr >pr' <plus_n_Sm_fast
    79 // qed.
     103  | S m ⇒ λpr': S m + part = ?.
     104    let postfix ≝ rvsplit … (\snd (vsplit bool (m*8) (S part*8) (offv (poff p) ⌈BitVector ?↦?⌉))) in
     105    (BVptr (pblock p) (mk_part … part …) postfix)::bevals_of_pointer_aux p (S part) m ?
     106  ].
     107@hide_prf
     108[3: change with (?*?) in match offset_size;
     109  <pr' >(commutative_times_fast ? 8) >(commutative_times_fast ? 8)
     110  <distributive_times_plus_fast <plus_n_Sm_fast %
     111] -postfix
     112/3 by lt_plus_to_minus_r, lt_plus_to_lt_l/ qed.
    80113
    81114definition bevals_of_pointer: pointer → list beval ≝
    82115 λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) ….
    83 // qed.
     116@hide_prf @plus_n_O qed.
    84117
    85118lemma pointer_of_bevals_bevals_of_pointer:
    86119 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
    87 * #pbl #poff
    88 try %
    89 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) (*[2,3: %]*)
    90 whd in ⊢ (??%?);(* >reflexive_eq_pointer >(eqb_n_n 2)*) %
     120* #pbl * #voff
     121whd in match (bevals_of_pointer ?);
     122@vsplit_elim #pre #post
     123normalize nodelta
     124#EQ >EQ
     125whd in match (bevals_of_pointer_aux ????);
     126@vsplit_elim #pre' #post'
     127normalize nodelta
     128>(Vector_O … pre') #EQ' normalize in EQ'; <EQ' -pre' -post'
     129whd in ⊢ (??%?);
     130>eq_block_b_b >eqb_n_n
     131>vflatten_rvsplit >vflatten_rvsplit
     132>vsuffix_true
     133[2: change with (bool_to_Prop (eq_bv ???)) >eq_bv_refl % ]
     134normalize nodelta %
    91135qed.
    92136
     
    137181 λv.match v with
    138182  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
     183  | BVnonzero ⇒ OK … true
    139184  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
    140185  | BVnull y ⇒  OK … false
    141   | BVptr p q ⇒ OK ? true ].
    142 
    143 axiom BadByte: String.
    144 
    145 definition Byte_of_val: beval → res Byte ≝ (*CSC: move elsewhere *)
    146  λb.match b with
     186  | BVptr p q o ⇒ OK ? true ].
     187
     188definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
     189 λerr,b.match b with
    147190  [ BVByte b ⇒ OK … b
    148   | _ ⇒ Error … [MSG BadByte]].
     191  | _ ⇒ Error … [MSG err]].
    149192
    150193axiom NotAnInt32Val: String.
     
    154197   match l with
    155198    [ nil ⇒ Error ? [MSG NotAnInt32Val]
    156     | cons hd tl ⇒ do b ← Byte_of_val hd ; OK ? 〈b,tl〉 ] in
     199    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
    157200  do 〈b1,l〉 ← first_byte l ;
    158201  do 〈b2,l〉 ← first_byte l ;
     
    163206    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
    164207
    165 (* CSC: maybe we should introduce a type of 1-bit-sized values *)
    166 definition BVtrue: beval ≝ BVByte [[false;false;false;false;false;false;false;true]].
    167 definition BVfalse: beval ≝ BVByte (zero …).
    168 definition beval_of_bool : bool → beval ≝ λb. if b then BVtrue else BVfalse.
    169 
    170 definition hw_register_env ≝ BitVectorTrie beval 6.
    171 definition empty_hw_register_env: hw_register_env ≝ Stub ….
    172 definition hwreg_retrieve: hw_register_env → Register → beval ≝
    173  λenv,r. lookup … (bitvector_of_register r) env BVundef.
    174 definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
    175  λr,v,env. insert … (bitvector_of_register r) v env.
     208inductive bebit : Type[0] ≝
     209| BBbit : bool → bebit
     210| BBundef : bebit
     211| BBptrcarry :
     212  (* is add *) bool → block → ∀p : part.Vector Byte (S p) → Vector Byte (S p) → bebit.
     213
     214definition eq_bebit: bebit → bebit → bool ≝
     215 λv1,v2.
     216  match v1 with
     217   [ BBundef      ⇒ match v2 with [ BBundef      ⇒ true                           | _ ⇒ false ]
     218   | BBbit b1    ⇒ match v2 with [ BBbit b2    ⇒ eq_b b1 b2                  | _ ⇒ false ]
     219   | BBptrcarry is_add1 b1 p1 o1 by1  ⇒
     220      match v2 with
     221      [ BBptrcarry is_add2 b2 p2 o2 by2  ⇒
     222        eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧
     223          (* equivalent to equality if p1 = p2 *)
     224          vprefix … (eq_bv 8) o1 o2 ∧
     225          vprefix … (eq_bv 8) by1 by2
     226      | _ ⇒ false
     227      ]
     228   ].
     229
     230definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
     231 λerr,b.match b with
     232  [ BBbit b ⇒ OK … b
     233  | _ ⇒ Error … [MSG err]].
Note: See TracChangeset for help on using the changeset viewer.